Toplevel.local_theory: proper target;
authorwenzelm
Thu Oct 12 22:57:15 2006 +0200 (2006-10-12)
changeset 209999131d8e96dba
parent 20998 714a08286899
child 21000 54c42dfbcafa
Toplevel.local_theory: proper target;
removed dead code;
src/HOL/Tools/function_package/fundef_datatype.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Oct 12 22:03:33 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Oct 12 22:57:15 2006 +0200
     1.3 @@ -14,8 +14,6 @@
     1.4      val setup : theory -> theory
     1.5  end
     1.6  
     1.7 -
     1.8 -
     1.9  structure FundefDatatype : FUNDEF_DATATYPE =
    1.10  struct
    1.11  
    1.12 @@ -167,6 +165,7 @@
    1.13      Proof.global_terminal_proof
    1.14        (Method.Basic (K pat_completeness),
    1.15         SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
    1.16 +         (* FIXME avoid dynamic scoping of method name! *)
    1.17  
    1.18  
    1.19  val setup =
    1.20 @@ -175,14 +174,9 @@
    1.21  
    1.22  
    1.23  
    1.24 -
    1.25 -
    1.26  local structure P = OuterParse and K = OuterKeyword in
    1.27  
    1.28  
    1.29 -fun local_theory_to_proof f = 
    1.30 -    Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
    1.31 -
    1.32  fun or_list1 s = P.enum1 "|" s
    1.33  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
    1.34  val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
    1.35 @@ -192,17 +186,12 @@
    1.36    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
    1.37    ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.38       >> (fn ((target, fixes), statements) =>
    1.39 -            Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements FundefCommon.fun_config 
    1.40 -                                                                                  #> by_pat_completeness_simp)));
    1.41 +            Toplevel.print o
    1.42 +            Toplevel.local_theory target
    1.43 +              (FundefPackage.add_fundef fixes statements FundefCommon.fun_config
    1.44 +               #> by_pat_completeness_simp)));
    1.45  
    1.46  val _ = OuterSyntax.add_parsers [funP];
    1.47  end
    1.48  
    1.49 -
    1.50 -
    1.51 -
    1.52 -
    1.53 -
    1.54 -
    1.55 -
    1.56  end