Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_set.ML
changeset 33766 c679f05600cd
parent 33671 4b0f2599ed48
child 34903 d75704c60768 
--- a/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -485,7 +485,7 @@
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
       |> Local_Theory.conceal  (* FIXME ?? *)
-      |> fold_map (Local_Theory.define "")
+      |> fold_map Local_Theory.define
         (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
isabelle