src/HOL/Tools/function_package/fundef_lib.ML

--- a/src/HOL/Tools/function_package/fundef_lib.ML	Fri Aug 08 09:26:15 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Fri Aug 08 09:44:16 2008 +0200
@@ -134,4 +134,12 @@
     |> rev
 
 
+datatype proof_attempt = Solved of thm | Stuck of thm | Fail
+
+fun try_proof cgoal tac = 
+    case SINGLE tac (Goal.init cgoal) of
+      NONE => Fail
+    | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
+
+
 end