# HG changeset patch
# User wenzelm
# Date 1433024267 -7200
# Node ID 05fabeb0130a04a18eb81c80de33fb9bc05cb408
# Parent  42079156c5aa94878c23a251b605cc532a3e3293
clarified context;

diff -r 42079156c5aa -r 05fabeb0130a src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sun May 31 00:16:26 2015 +0200
+++ b/src/Tools/nbe.ML	Sun May 31 00:17:47 2015 +0200
@@ -86,13 +86,12 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val algebra = Sign.classes_of thy;
-    val certT = Thm.global_ctyp_of thy;
     val triv_classes = get_triv_classes thy;
     fun additional_classes sort = filter_out (fn class => Sorts.sort_le algebra (sort, [class])) triv_classes;
     fun mk_entry (v, sort) =
       let
         val T = TFree (v, sort);
-        val cT = certT T;
+        val cT = Thm.ctyp_of ctxt T;
         val triv_sort = additional_classes sort;
       in
         (v, (Sorts.inter_sort algebra (sort, triv_sort),
@@ -102,14 +101,14 @@
     val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []);
     fun instantiate thm =
       let
-        val cert_tvars = map (certT o TVar) (Term.add_tvars
+        val cert_tvars = map (Thm.ctyp_of ctxt o TVar) (Term.add_tvars
           ((fst o Logic.dest_equals o Logic.strip_imp_concl o Thm.prop_of) thm) []);
         val instantiation =
           map2 (fn cert_tvar => fn (_, (_, (cT, _))) => (cert_tvar, cT)) cert_tvars vs_tab;
       in Thm.instantiate (instantiation, []) thm end;
     fun of_class (TFree (v, _), class) =
           the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class)
-      | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ_global thy T);
+      | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T);
     fun strip_of_class thm =
       let
         val prems_of_class = Thm.prop_of thm
@@ -118,8 +117,10 @@
       in fold Thm.elim_implies prems_of_class thm end;
   in
     ct
-    |> (Drule.cterm_fun o map_types o map_type_tfree)
+    |> Thm.term_of
+    |> (map_types o map_type_tfree)
         (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
+    |> Thm.cterm_of ctxt
     |> conv
     |> Thm.strip_shyps
     |> Thm.varifyT_global