src/Tools/IsaPlanner/isand.ML
changeset 59641 a2d056424d3c
parent 59621 291934bac95e
child 60358 aebfbcab1eb8
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Fri Mar 06 23:55:04 2015 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Fri Mar 06 23:55:55 2015 +0100
     1.3 @@ -91,10 +91,9 @@
     1.4  
     1.5  fun fix_alls_cterm ctxt i th =
     1.6    let
     1.7 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
     1.8      val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
     1.9 -    val cfvs = rev (map cert fvs);
    1.10 -    val ct_body = cert fixedbody;
    1.11 +    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
    1.12 +    val ct_body = Thm.cterm_of ctxt fixedbody;
    1.13    in (ct_body, cfvs) end;
    1.14  
    1.15  fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
    1.16 @@ -140,12 +139,12 @@
    1.17  *)
    1.18  fun subgoal_thms th =
    1.19    let
    1.20 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
    1.21 +    val thy = Thm.theory_of_thm th;
    1.22  
    1.23      val t = Thm.prop_of th;
    1.24  
    1.25      val prems = Logic.strip_imp_prems t;
    1.26 -    val aprems = map (Thm.trivial o cert) prems;
    1.27 +    val aprems = map (Thm.trivial o Thm.global_cterm_of thy) prems;
    1.28  
    1.29      fun explortf premths = Drule.implies_elim_list th premths;
    1.30    in (aprems, explortf) end;