src/HOL/Tools/function_package/fundef_datatype.ML

     val pat_complete_tac: int -> tactic
 
     val pat_completeness : method
     val setup : theory -> theory
 end
-
-
 
 structure FundefDatatype : FUNDEF_DATATYPE =
 struct
 
 

 
 val by_pat_completeness_simp =
     Proof.global_terminal_proof
       (Method.Basic (K pat_completeness),
        SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
+         (* FIXME avoid dynamic scoping of method name! *)
 
 
 val setup =
     Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]
 
 
 
 
-
-
 local structure P = OuterParse and K = OuterKeyword in
 
-
-fun local_theory_to_proof f = 
-    Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
 
 fun or_list1 s = P.enum1 "|" s
 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
 val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
 val statements_ow = or_list1 statement_ow
 
 val funP =
   OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
   ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
      >> (fn ((target, fixes), statements) =>
-            Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements FundefCommon.fun_config 
-                                                                                  #> by_pat_completeness_simp)));
+            Toplevel.print o
+            Toplevel.local_theory target
+              (FundefPackage.add_fundef fixes statements FundefCommon.fun_config
+               #> by_pat_completeness_simp)));
 
 val _ = OuterSyntax.add_parsers [funP];
 end
 
-
-
-
-
-
-
-
 end