src/Tools/IsaPlanner/isand.ML
changeset 59582 0fbed69ff081
parent 52467 24c6ddb48cb8
child 59621 291934bac95e
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -142,7 +142,7 @@
     1.4    let
     1.5      val cert = Thm.cterm_of (Thm.theory_of_thm th);
     1.6  
     1.7 -    val t = prop_of th;
     1.8 +    val t = Thm.prop_of th;
     1.9  
    1.10      val prems = Logic.strip_imp_prems t;
    1.11      val aprems = map (Thm.trivial o cert) prems;