src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 59636 9f44d053b972
parent 59621 291934bac95e
child 60367 e201bd8973db
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 23:52:57 2015 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 23:53:36 2015 +0100
     1.3 @@ -869,7 +869,7 @@
     1.4  
     1.5  fun expand_tuples thy intro =
     1.6    let
     1.7 -    val ctxt = Proof_Context.init_global thy
     1.8 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     1.9      val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
    1.10      val intro_t = Thm.prop_of intro'
    1.11      val concl = Logic.strip_imp_concl intro_t
    1.12 @@ -877,7 +877,7 @@
    1.13      val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
    1.14      val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
    1.15      fun rewrite_pat (ct1, ct2) =
    1.16 -      (ct1, Thm.global_cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
    1.17 +      (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
    1.18      val t_insts' = map rewrite_pat t_insts
    1.19      val intro'' = Thm.instantiate (T_insts, t_insts') intro
    1.20      val [intro'''] = Variable.export ctxt3 ctxt [intro'']