clarified context;
authorwenzelm
Fri Mar 06 23:53:36 2015 +0100 (2015-03-06)
changeset 596369f44d053b972
parent 59635 025f70f35daf
child 59637 f643308472ce
clarified context;
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Mar 06 23:52:57 2015 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Mar 06 23:53:36 2015 +0100
     1.3 @@ -235,7 +235,7 @@
     1.4          fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t)
     1.5          fun inst_of_matches tts =
     1.6            fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
     1.7 -          |> snd |> Vartab.dest |> map (apply2 (Thm.global_cterm_of thy) o term_pair_of)
     1.8 +          |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of ctxt2) o term_pair_of)
     1.9          val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems)
    1.10          val case_th =
    1.11            rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 23:52:57 2015 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 23:53:36 2015 +0100
     2.3 @@ -869,7 +869,7 @@
     2.4  
     2.5  fun expand_tuples thy intro =
     2.6    let
     2.7 -    val ctxt = Proof_Context.init_global thy
     2.8 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     2.9      val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
    2.10      val intro_t = Thm.prop_of intro'
    2.11      val concl = Logic.strip_imp_concl intro_t
    2.12 @@ -877,7 +877,7 @@
    2.13      val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
    2.14      val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
    2.15      fun rewrite_pat (ct1, ct2) =
    2.16 -      (ct1, Thm.global_cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
    2.17 +      (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
    2.18      val t_insts' = map rewrite_pat t_insts
    2.19      val intro'' = Thm.instantiate (T_insts, t_insts') intro
    2.20      val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 06 23:52:57 2015 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 06 23:53:36 2015 +0100
     3.3 @@ -143,7 +143,7 @@
     3.4  
     3.5  fun introrulify thy ths = 
     3.6    let
     3.7 -    val ctxt = Proof_Context.init_global thy
     3.8 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     3.9      val ((_, ths'), ctxt') = Variable.import true ths ctxt
    3.10      fun introrulify' th =
    3.11        let
    3.12 @@ -158,14 +158,15 @@
    3.13            in
    3.14              (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
    3.15            end
    3.16 -        val x = (Thm.global_cterm_of thy o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
    3.17 -          Logic.dest_implies o Thm.prop_of) @{thm exI}
    3.18 +        val x =
    3.19 +          (Thm.cterm_of ctxt' o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
    3.20 +            Logic.dest_implies o Thm.prop_of) @{thm exI}
    3.21          fun prove_introrule (index, (ps, introrule)) =
    3.22            let
    3.23              val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
    3.24                THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
    3.25                THEN (EVERY (map (fn y =>
    3.26 -                rtac (Drule.cterm_instantiate [(x, Thm.global_cterm_of thy (Free y))] @{thm exI}) 1) ps))
    3.27 +                rtac (Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}) 1) ps))
    3.28                THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
    3.29                THEN TRY (assume_tac ctxt' 1)
    3.30            in