src/HOL/Tools/function_package/fundef_datatype.ML
changeset 24867 e5b55d7be9bb
parent 24466 619f78b717cb
child 24920 2a45e400fdad
     1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -302,13 +302,12 @@
     1.4        |> by_pat_completeness_simp
     1.5        |> termination_by_lexicographic_order
     1.6  
     1.7 -val funP =
     1.8 +val _ =
     1.9    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
    1.10    (fundef_parser fun_config
    1.11       >> (fn ((config, fixes), (flags, statements)) =>
    1.12              (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
    1.13  
    1.14 -val _ = OuterSyntax.add_parsers [funP];
    1.15  end
    1.16  
    1.17  end