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.
IsarThy.theorems_i;
authorwenzelm
Fri, 11 Jan 2002 00:35:03 +0100
changeset 12716 fa4ea2856a31
parent 12715 f7299128cd7d
child 12717 2d6b5e22e05d
IsarThy.theorems_i;
src/ZF/Tools/ind_cases.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/Tools/ind_cases.ML	Fri Jan 11 00:34:43 2002 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Jan 11 00:35:03 2002 +0100
@@ -55,9 +55,9 @@
     val read_prop = ProofContext.read_prop (ProofContext.init thy);
     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
     val facts = args |> map (fn ((name, srcs), props) =>
-      (((name, map (Attrib.global_attribute thy) srcs), map (Thm.no_attributes o mk_cases) props),
-        Comment.none));
-  in thy |> IsarThy.have_theorems_i Drule.lemmaK facts end;
+      (((name, map (Attrib.global_attribute thy) srcs),
+        map (Thm.no_attributes o single o mk_cases) props), Comment.none));
+  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
 
 
 (* ind_cases method *)
isabelle