src/Pure/goal.ML
changeset 22902 ac833b4bb7ee
parent 21687 f689f729afab
child 23237 ac9d126456e1
     1.1 --- a/src/Pure/goal.ML	Thu May 10 00:39:46 2007 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu May 10 00:39:48 2007 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4    C ==> #C
     1.5  *)
     1.6  val init =
     1.7 -  let val A = #1 (Drule.dest_implies (Thm.cprop_of Drule.protectI))
     1.8 +  let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI))
     1.9    in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
    1.10  
    1.11  (*