src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -896,7 +896,7 @@
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
-      |> TheoryTarget.init NONE
+      |> Theory_Target.init NONE
       |> LocalTheory.set_group group
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> LocalTheory.exit;