src/HOL/Tools/inductive_set.ML
changeset 33766 c679f05600cd
parent 33671 4b0f2599ed48
child 34903 d75704c60768
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:45:56 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:46:33 2009 +0100
     1.3 @@ -485,7 +485,7 @@
     1.4      (* define inductive sets using previously defined predicates *)
     1.5      val (defs, lthy2) = lthy1
     1.6        |> Local_Theory.conceal  (* FIXME ?? *)
     1.7 -      |> fold_map (Local_Theory.define "")
     1.8 +      |> fold_map Local_Theory.define
     1.9          (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    1.10             fold_rev lambda params (HOLogic.Collect_const U $
    1.11               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))