src/HOL/Tools/Function/fun.ML

--- a/src/HOL/Tools/Function/fun.ML	Fri Nov 13 20:41:29 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Fri Nov 13 21:11:15 2009 +0100
@@ -153,11 +153,11 @@
 fun gen_fun add config fixes statements int lthy =
   let val group = serial () in
     lthy
-      |> LocalTheory.set_group group
+      |> Local_Theory.set_group group
       |> add fixes statements config
       |> by_pat_completeness_auto int
-      |> LocalTheory.restore
-      |> LocalTheory.set_group group
+      |> Local_Theory.restore
+      |> Local_Theory.set_group group
       |> termination_by (Function_Common.get_termination_prover lthy) int
   end;