src/Pure/Isar/find_theorems.ML
changeset 18939 18e2a2676d80
parent 18325 2d504ea54e5b
child 19046 bc5c6c9b114e
--- a/src/Pure/Isar/find_theorems.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -139,7 +139,7 @@
     val concl = Logic.concl_of_goal goal 1;
     val ss = is_matching_thm extract_intro ctxt true concl thm;
   in
-    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
+    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   end;
 
 fun filter_elim ctxt goal (_, thm) =
@@ -176,7 +176,7 @@
       (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
     val ss = is_matching_thm extract_simp ctxt false t thm
   in
-    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
+    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   end;