1.1 --- a/src/Tools/Compute_Oracle/compute.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -391,9 +391,9 @@
     1.4  fun export_thm thy hyps shyps prop =
     1.5      let
     1.6          val th = export_oracle (thy, hyps, shyps, prop)
     1.7 -        val hyps = map (fn h => assume (cterm_of thy h)) hyps
     1.8 +        val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
     1.9      in
    1.10 -        fold (fn h => fn p => implies_elim p h) hyps th 
    1.11 +        fold (fn h => fn p => Thm.implies_elim p h) hyps th 
    1.12      end
    1.13          
    1.14  (* --------- Rewrite ----------- *)