src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
changeset 60781 2da59cdf531c
parent 60752 b48830b670a1
child 61268 abe08fb15a12
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -141,9 +141,8 @@
     1.4      (intros'', (local_defs, thy'))
     1.5    end
     1.6  
     1.7 -fun introrulify thy ths = 
     1.8 +fun introrulify ctxt ths = 
     1.9    let
    1.10 -    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
    1.11      val ((_, ths'), ctxt') = Variable.import true ths ctxt
    1.12      fun introrulify' th =
    1.13        let
    1.14 @@ -158,8 +157,8 @@
    1.15            in
    1.16              (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
    1.17            end
    1.18 -        val x =
    1.19 -          (Thm.cterm_of ctxt' o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
    1.20 +        val Var (x, _) =
    1.21 +          (the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
    1.22              Logic.dest_implies o Thm.prop_of) @{thm exI}
    1.23          fun prove_introrule (index, (ps, introrule)) =
    1.24            let
    1.25 @@ -167,7 +166,7 @@
    1.26                THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
    1.27                THEN (EVERY (map (fn y =>
    1.28                  resolve_tac ctxt'
    1.29 -                  [Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
    1.30 +                  [infer_instantiate ctxt' [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
    1.31                THEN REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 THEN assume_tac ctxt' 1)
    1.32                THEN TRY (assume_tac ctxt' 1)
    1.33            in
    1.34 @@ -205,7 +204,7 @@
    1.35        val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
    1.36        val intros =
    1.37          if forall is_pred_equation specs then 
    1.38 -          map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
    1.39 +          map (split_conjuncts_in_assms ctxt) (introrulify ctxt (map (rewrite ctxt) specs))
    1.40          else if forall (is_intro constname) specs then
    1.41            map (rewrite_intros ctxt) specs
    1.42          else