src/Tools/IsaPlanner/isand.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59641 a2d056424d3c
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4  
     1.5  fun fix_alls_cterm ctxt i th =
     1.6    let
     1.7 -    val cert = Thm.cterm_of (Thm.theory_of_thm th);
     1.8 +    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
     1.9      val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
    1.10      val cfvs = rev (map cert fvs);
    1.11      val ct_body = cert fixedbody;
    1.12 @@ -140,7 +140,7 @@
    1.13  *)
    1.14  fun subgoal_thms th =
    1.15    let
    1.16 -    val cert = Thm.cterm_of (Thm.theory_of_thm th);
    1.17 +    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
    1.18  
    1.19      val t = Thm.prop_of th;
    1.20