src/Tools/nbe.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59642 929984c529d3
     1.1 --- a/src/Tools/nbe.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Tools/nbe.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4  
     1.5  val (_, triv_of_class) = Context.>>> (Context.map_theory_result
     1.6    (Thm.add_oracle (@{binding triv_of_class}, fn (thy, T, class) =>
     1.7 -    Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
     1.8 +    Thm.global_cterm_of thy (Logic.mk_of_class (T, class)))));
     1.9  
    1.10  in
    1.11  
    1.12 @@ -86,7 +86,7 @@
    1.13    let
    1.14      val thy = Proof_Context.theory_of ctxt;
    1.15      val algebra = Sign.classes_of thy;
    1.16 -    val certT = Thm.ctyp_of thy;
    1.17 +    val certT = Thm.global_ctyp_of thy;
    1.18      val triv_classes = get_triv_classes thy;
    1.19      fun additional_classes sort = filter_out (fn class => Sorts.sort_le algebra (sort, [class])) triv_classes;
    1.20      fun mk_entry (v, sort) =
    1.21 @@ -582,8 +582,8 @@
    1.22    let
    1.23      val thy = Proof_Context.theory_of ctxt;
    1.24      val ty = Thm.typ_of_cterm lhs;
    1.25 -    val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
    1.26 -    val rhs = Thm.cterm_of thy raw_rhs;
    1.27 +    val eq = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
    1.28 +    val rhs = Thm.global_cterm_of thy raw_rhs;
    1.29    in Thm.mk_binop eq lhs rhs end;
    1.30  
    1.31  val (_, raw_oracle) = Context.>>> (Context.map_theory_result