src/HOL/Matrix_LP/Compute_Oracle/compute.ML

     end)));
 
 fun export_thm thy hyps shyps prop =
     let
         val th = export_oracle (thy, hyps, shyps, prop)
-        val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
+        val hyps = map (fn h => Thm.assume (Thm.cterm_of thy h)) hyps
     in
         fold (fn h => fn p => Thm.implies_elim p h) hyps th 
     end
         
 (* --------- Rewrite ----------- *)
 
 fun rewrite computer ct =
     let
         val thy = Thm.theory_of_cterm ct
-        val {t=t',T=ty,...} = rep_cterm ct
+        val {t=t',T=ty,...} = Thm.rep_cterm ct
         val _ = super_theory (theory_of computer) thy
         val naming = naming_of computer
         val (encoding, t) = remove_types (encoding_of computer) t'
         val t = runprog (prog_of computer) t
         val t = infer_types naming encoding ty t

 
 exception ParamSimplify of computer * theorem
 
 fun make_theorem computer th vars =
 let
-    val _ = super_theory (theory_of computer) (theory_of_thm th)
+    val _ = super_theory (theory_of computer) (Thm.theory_of_thm th)
 
     val (ComputeThm (hyps, shyps, prop)) = thm2cthm th 
 
     val encoding = encoding_of computer
  

             case mk_prem encoding t  of 
                 (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, []))
     val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop)
     val _ = set_encoding computer encoding
 in
-    Theorem (theory_of_thm th, stamp_of computer, vartab, varsubst, 
+    Theorem (Thm.theory_of_thm th, stamp_of computer, vartab, varsubst, 
              prems, concl, hyps, shyps)
 end
     
 fun theory_of_theorem (Theorem (thy,_,_,_,_,_,_,_)) = thy
 fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = Theorem (thy,p0,p1,p2,p3,p4,p5,p6)

         else 
             raise Compute "instantiate: not a closed term"
 
     fun compute_inst (s, ct) vs =
         let
-            val _ = super_theory (theory_of_cterm ct) thy
-            val ty = typ_of (ctyp_of_term ct) 
+            val _ = super_theory (Thm.theory_of_cterm ct) thy
+            val ty = Thm.typ_of (Thm.ctyp_of_term ct) 
         in          
             (case Symtab.lookup vartab s of 
                  NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
                | SOME (x, ty') => 
                  (case Inttab.lookup vs x of 

                     | SOME NONE => 
                       if ty <> ty' then 
                           raise Compute ("instantiate: wrong type for variable '"^s^"'")
                       else
                           let
-                              val t = rewrite computer (term_of ct)
+                              val t = rewrite computer (Thm.term_of ct)
                               val _ = assert_varfree vs t 
                               val _ = assert_closed t
                           in
                               Inttab.update (x, SOME t) vs
                           end

 let
     val _ = check_compatible computer th
     val thy = 
         let
             val thy1 = theory_of_theorem th
-            val thy2 = theory_of_thm th'
+            val thy2 = Thm.theory_of_thm th'
         in
             if Theory.subthy (thy1, thy2) then thy2 
             else if Theory.subthy (thy2, thy1) then thy1 else
             raise Compute "modus_ponens: theorems are not compatible with each other"
         end