Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changed type of Logic.strip_horn.
authorberghofe
Mon, 21 Oct 2002 16:57:39 +0200
changeset 13656 58bb243dbafb
parent 13655 95b95cdb4704
child 13657 c1637d60a846
Changed type of Logic.strip_horn.
src/HOL/Tools/datatype_realizer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Oct 18 17:50:13 2002 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 21 16:57:39 2002 +0200
@@ -29,7 +29,7 @@
 
 fun prove_goal' sg p f =
   let
-    val (_, As, B) = Logic.strip_horn p;
+    val (As, B) = Logic.strip_horn p;
     val cAs = map (cterm_of sg) As;
     val asms = map (norm_hhf_rule o assume) cAs;
     fun check thm = if nprems_of thm > 0 then
isabelle