src/Tools/IsaPlanner/rw_inst.ML
changeset 60358 aebfbcab1eb8
parent 59641 a2d056424d3c
child 60642 48dd1cefb4ae
     1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -30,15 +30,13 @@
     1.4  th: A vs ==> B vs
     1.5  Results in: "B vs" [!!x. A x]
     1.6  *)
     1.7 -fun allify_conditions Ts th =
     1.8 +fun allify_conditions ctxt Ts th =
     1.9    let
    1.10 -    val thy = Thm.theory_of_thm th;
    1.11 -
    1.12      fun allify (x, T) t =
    1.13        Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
    1.14  
    1.15 -    val cTs = map (Thm.global_cterm_of thy o Free) Ts;
    1.16 -    val cterm_asms = map (Thm.global_cterm_of thy o fold_rev allify Ts) (Thm.prems_of th);
    1.17 +    val cTs = map (Thm.cterm_of ctxt o Free) Ts;
    1.18 +    val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th);
    1.19      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
    1.20    in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    1.21  
    1.22 @@ -82,7 +80,7 @@
    1.23        |> Drule.forall_elim_list tonames;
    1.24  
    1.25      (* make unconditional rule and prems *)
    1.26 -    val (uncond_rule, cprems) = allify_conditions (rev Ts') rule';
    1.27 +    val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule';
    1.28  
    1.29      (* using these names create lambda-abstracted version of the rule *)
    1.30      val abstractions = rev (Ts' ~~ tonames);