src/HOL/Tools/inductive_set.ML
changeset 33643 b275f26a638b
parent 33519 e31a85f92ce9
child 33669 ae9a2ea9a989
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Nov 12 21:59:35 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 12 22:02:11 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        |> LocalTheory.conceal  (* FIXME ?? *)
     1.7 -      |> fold_map (LocalTheory.define Thm.internalK)
     1.8 +      |> fold_map (LocalTheory.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))))))