src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59636 9f44d053b972
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -877,7 +877,7 @@
     1.4      val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
     1.5      val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
     1.6      fun rewrite_pat (ct1, ct2) =
     1.7 -      (ct1, Thm.cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
     1.8 +      (ct1, Thm.global_cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
     1.9      val t_insts' = map rewrite_pat t_insts
    1.10      val intro'' = Thm.instantiate (T_insts, t_insts') intro
    1.11      val [intro'''] = Variable.export ctxt3 ctxt [intro'']