1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 07 01:31:02 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 07 01:31:03 2006 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4  
     1.5  
     1.6  fun local_theory_to_proof f = 
     1.7 -    Toplevel.theory_to_proof (f o LocalTheory.init NONE)
     1.8 +    Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
     1.9  
    1.10  fun or_list1 s = P.enum1 "|" s
    1.11  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
    1.12 @@ -205,4 +205,4 @@
    1.13  
    1.14  
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end