src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -998,7 +998,7 @@
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
-      |> Named_Target.init NONE
+      |> Named_Target.theory_init
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> Local_Theory.exit;
     val info = #2 (the_inductive ctxt' name);