# HG changeset patch
# User wenzelm
# Date 1236891062 -3600
# Node ID 9cdc7ce0e3891268094611a9e5f357c961c700cd
# Parent  99def5248e7fb8cd18c10d9890b0ad5d84d33ae1
simplified preparation and outer parsing of specification;

diff -r 99def5248e7f -r 9cdc7ce0e389 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 12 21:47:36 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 12 21:51:02 2009 +0100
@@ -359,7 +359,7 @@
                          >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
 in
   fun fundef_parser default_cfg = 
-      config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements
+      config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements
 end
 
 
diff -r 99def5248e7f -r 9cdc7ce0e389 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 12 21:47:36 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 12 21:51:02 2009 +0100
@@ -93,13 +93,12 @@
     end
 
 
-fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
     let
       val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
-      val ((fixes0, spec0), ctxt') = 
-        prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
+      val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
       val fixes = map (apfst (apfst Binding.name_of)) fixes0;
-      val spec = map (apfst (apfst Binding.name_of)) spec0;
+      val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
 
       val defname = mk_defname fixes
@@ -163,9 +162,8 @@
   |> LocalTheory.set_group (serial_string ())
   |> setup_termination_proof term_opt;
 
-val add_fundef = gen_add_fundef true Specification.read_specification "_::type"
-val add_fundef_i = 
-  gen_add_fundef false Specification.check_specification (TypeInfer.anyT HOLogic.typeS)
+val add_fundef = gen_add_fundef true Specification.read_spec "_::type"
+val add_fundef_i = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
 
 
 (* Datatype hook to declare datatype congs as "fundef_congs" *)
diff -r 99def5248e7f -r 9cdc7ce0e389 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Mar 12 21:47:36 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 12 21:51:02 2009 +0100
@@ -842,11 +842,10 @@
 
 fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
   let
-    val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
-      |> Specification.read_specification
-          (cnames_syn @ pnames_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs);
+    val ((vars, intrs), _) = lthy
+      |> ProofContext.set_mode ProofContext.mode_abbrev
+      |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
     val (cs, ps) = chop (length cnames_syn) vars;
-    val intrs = map (apsnd the_single) specs;
     val monos = Attrib.eval_thms lthy raw_monos;
     val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
       alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
@@ -946,22 +945,12 @@
 
 val _ = OuterKeyword.keyword "monos";
 
-(* FIXME eliminate *)
-fun flatten_specification specs = specs |> maps
-  (fn (a, (concl, [])) => concl |> map
-        (fn ((b, atts), [B]) =>
-              if Binding.is_empty a then ((b, atts), B)
-              else if Binding.is_empty b then ((a, atts), B)
-              else error "Illegal nested case names"
-          | ((b, _), _) => error "Illegal simultaneous specification")
-    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.str_of a)));
-
 fun gen_ind_decl mk_def coind =
   P.fixes -- P.for_fixes --
-  Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
+  Scan.optional SpecParse.where_alt_specs [] --
   Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
-      (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
+      (snd oo gen_add_inductive mk_def true coind preds params specs monos));
 
 val ind_decl = gen_ind_decl add_ind_def;
 
@@ -971,7 +960,7 @@
 val _ =
   OuterSyntax.local_theory "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 SpecParse.spec >> (fn specs => snd o inductive_cases specs));
+    (P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
 
 end;