src/Tools/IsaPlanner/isand.ML
changeset 60358 aebfbcab1eb8
parent 59641 a2d056424d3c
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -137,14 +137,12 @@
     1.4   ["SG0", ..., "SGm"] : thm list ->   -- export function
     1.5     "G" : thm)
     1.6  *)
     1.7 -fun subgoal_thms th =
     1.8 +fun subgoal_thms ctxt th =
     1.9    let
    1.10 -    val thy = Thm.theory_of_thm th;
    1.11 -
    1.12      val t = Thm.prop_of th;
    1.13  
    1.14      val prems = Logic.strip_imp_prems t;
    1.15 -    val aprems = map (Thm.trivial o Thm.global_cterm_of thy) prems;
    1.16 +    val aprems = map (Thm.trivial o Thm.cterm_of ctxt) prems;
    1.17  
    1.18      fun explortf premths = Drule.implies_elim_list th premths;
    1.19    in (aprems, explortf) end;
    1.20 @@ -167,7 +165,7 @@
    1.21  (* requires being given solutions! *)
    1.22  fun fixed_subgoal_thms ctxt th =
    1.23    let
    1.24 -    val (subgoals, expf) = subgoal_thms th;
    1.25 +    val (subgoals, expf) = subgoal_thms ctxt th;
    1.26  (*  fun export_sg (th, exp) = exp th; *)
    1.27      fun export_sgs expfs solthms =
    1.28        expf (map2 (curry (op |>)) solthms expfs);