# HG changeset patch
# User wenzelm
# Date 1236892585 -3600
# Node ID d09b7f0c2c140549cb87ac916400e68df0d33c47
# Parent  5d7d0add17410719bd8a27bb0659ed116550f3f2# Parent  a14ff49d30830b7b7349e2b49fc30e172acc912a
merged

diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/FunDef.thy	Thu Mar 12 22:16:25 2009 +0100
@@ -314,13 +314,11 @@
 use "Tools/function_package/scnp_reconstruct.ML"
 
 setup {* ScnpReconstruct.setup *}
-(*
-setup {*
+
+ML_val -- "setup inactive"
+{*
   Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
   [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
 *}
-*)
-
-
 
 end
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Import/shuffler.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -662,7 +662,7 @@
 fun search_meth ctxt =
     let
         val thy = ProofContext.theory_of ctxt
-        val prems = Assumption.prems_of ctxt
+        val prems = Assumption.all_prems_of ctxt
     in
         Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
     end
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -12,6 +12,10 @@
     (binding * typ option * mixfix) list ->
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> Proof.state
+  val add_primrec_cmd: string list option -> string option ->
+    (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
+    (Attrib.binding * string) list -> local_theory -> Proof.state
 end;
 
 structure NominalPrimrec : NOMINAL_PRIMREC =
@@ -36,10 +40,10 @@
       (fn Free (v, _) => insert (op =) v | _ => I) body []))
   in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
 
-fun process_eqn lthy is_fixed spec rec_fns = 
+fun process_eqn lthy is_fixed spec rec_fns =
   let
     val eq = unquantify spec;
-    val (lhs, rhs) = 
+    val (lhs, rhs) =
       HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
       handle TERM _ => raise RecError "not a proper equation";
 
@@ -67,7 +71,7 @@
     fun check_vars _ [] = ()
       | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
   in
-    if length middle > 1 then 
+    if length middle > 1 then
       raise RecError "more than one non-variable in pattern"
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
@@ -159,7 +163,7 @@
               val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
                 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
                   handle RecError s => primrec_eq_err lthy s eq
-            in (fnames'', fnss'', 
+            in (fnames'', fnss'',
                 (list_abs_free (cargs' @ subs, rhs'))::fns)
             end)
 
@@ -172,7 +176,7 @@
             val SOME (_, _, eqns' as (_, (ls, _, rs, _, _)) :: _) =
               AList.lookup (op =) eqns fname;
             val (fnames', fnss', fns) = fold_rev (trans eqns') constrs
-              ((i, fname)::fnames, fnss, []) 
+              ((i, fname)::fnames, fnss, [])
           in
             (fnames', (i, (fname, ls, rs, fns))::fnss')
           end
@@ -235,15 +239,9 @@
 
 local
 
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
-  let
-    val ((fixes, spec), _) = prep_spec
-      raw_fixes (map (single o apsnd single) raw_spec) ctxt
-  in (fixes, map (apsnd the_single) spec) end;
-
 fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
   let
-    val (fixes', spec) = prepare_spec prep_spec lthy (raw_fixes @ raw_params) raw_spec;
+    val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
     val fixes = List.take (fixes', length raw_fixes);
     val (names_atts, spec') = split_list spec;
     val eqns' = map unquantify spec'
@@ -261,12 +259,12 @@
        then () else primrec_err param_err);
     val tnames = distinct (op =) (map (#1 o snd) eqns);
     val dts = find_dts dt_info tnames tnames;
-    val main_fns = 
+    val main_fns =
       map (fn (tname, {index, ...}) =>
-        (index, 
+        (index,
           (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns))
       dts;
-    val {descr, rec_names, rec_rewrites, ...} = 
+    val {descr, rec_names, rec_rewrites, ...} =
       if null dts then
         primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
       else snd (hd dts);
@@ -388,15 +386,15 @@
 
 in
 
-val add_primrec = gen_primrec false Specification.check_specification (K I);
-val add_primrec_cmd = gen_primrec true Specification.read_specification Syntax.read_term;
+val add_primrec = gen_primrec false Specification.check_spec (K I);
+val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
 
 end;
 
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = OuterParse in
 
 val freshness_context = P.reserved "freshness_context";
 val invariant = P.reserved "invariant";
@@ -408,28 +406,16 @@
     (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
   (parser1 >> pair NONE);
 val options =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-    (parser2 --| P.$$$ ")")) (NONE, NONE);
-
-fun pipe_error t = P.!!! (Scan.fail_with (K
-  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
-  ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-val statements = P.enum1 "|" statement;
-
-val primrec_decl = P.opt_target -- options --
-  P.fixes -- P.for_fixes --| P.$$$ "where" -- statements;
+  Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
 
 val _ =
-  OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
-    (primrec_decl >> (fn ((((opt_target, (invs, fctxt)), raw_fixes), raw_params), raw_spec) =>
-      Toplevel.print o Toplevel.local_theory_to_proof opt_target
-        (add_primrec_cmd invs fctxt raw_fixes raw_params raw_spec)));
+  OuterSyntax.local_theory_to_proof "nominal_primrec"
+    "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
+    (options -- P.fixes -- P.for_fixes -- SpecParse.where_alt_specs
+      >> (fn ((((invs, fctxt), fixes), params), specs) =>
+        add_primrec_cmd invs fctxt fixes params specs));
 
 end;
 
-
 end;
 
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Statespace/state_space.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -419,7 +419,7 @@
         val expr = ([(suffix valuetypesN name, 
                      (("",false),Expression.Positional (map SOME pars)))],[]);
       in
-        prove_interpretation_in (ALLGOALS o solve_tac o Assumption.prems_of)
+        prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
           (suffix valuetypesN name, expr) thy
       end;
 
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 12 22:16:25 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 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 12 22:16:25 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 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 12 22:16:25 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;
 
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/primrec_package.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -9,6 +9,8 @@
 sig
   val add_primrec: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> thm list * local_theory
+  val add_primrec_cmd: (binding * string option * mixfix) list ->
+    (Attrib.binding * string) list -> local_theory -> thm list * local_theory
   val add_primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> thm list * theory
   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
@@ -213,12 +215,6 @@
 
 local
 
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
-  let
-    val ((fixes, spec), _) = prep_spec
-      raw_fixes (map (single o apsnd single) raw_spec) ctxt
-  in (fixes, map (apsnd the_single) spec) end;
-
 fun prove_spec ctxt names rec_rewrites defs eqs =
   let
     val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
@@ -228,7 +224,7 @@
 
 fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
   let
-    val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
+    val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
     val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
       orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
     val tnames = distinct (op =) (map (#1 o snd) eqns);
@@ -268,8 +264,8 @@
 
 in
 
-val add_primrec = gen_primrec false Specification.check_specification;
-val add_primrec_cmd = gen_primrec true Specification.read_specification;
+val add_primrec = gen_primrec false Specification.check_spec;
+val add_primrec_cmd = gen_primrec true Specification.read_spec;
 
 end;
 
@@ -300,24 +296,16 @@
 val old_primrec_decl =
   opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
 
-fun pipe_error t = P.!!! (Scan.fail_with (K
-  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
-  ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-val statements = P.enum1 "|" statement;
-
-val primrec_decl = P.opt_target -- P.fixes --| P.$$$ "where" -- statements;
+val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
 
 val _ =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    ((primrec_decl >> (fn ((opt_target, raw_fixes), raw_spec) =>
-      Toplevel.local_theory opt_target (add_primrec_cmd raw_fixes raw_spec #> snd)))
+    ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
+      Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
     || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
       Toplevel.theory (snd o
-        (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec) alt_name
-          (map P.triple_swap eqns)))));
+        (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec)
+          alt_name (map P.triple_swap eqns)))));
 
 end;
 
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOLCF/Tools/domain/domain_axioms.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -108,7 +108,16 @@
     [take_def, finite_def])
 end; (* let (calc_axioms) *)
 
-fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
+
+(* legacy type inference *)
+
+fun legacy_infer_term thy t =
+  singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+
+fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+
+fun infer_props thy = map (apsnd (legacy_infer_prop thy));
+
 
 fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOLCF/Tools/fixrec_package.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -6,17 +6,12 @@
 
 signature FIXREC_PACKAGE =
 sig
-  val legacy_infer_term: theory -> term -> term
-  val legacy_infer_prop: theory -> term -> term
-
-  val add_fixrec: bool -> (binding * string option * mixfix) list
+  val add_fixrec: bool -> (binding * typ option * mixfix) list
+    -> (Attrib.binding * term) list -> local_theory -> local_theory
+  val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
     -> (Attrib.binding * string) list -> local_theory -> local_theory
-
-  val add_fixrec_i: bool -> (binding * typ option * mixfix) list
-    -> (Attrib.binding * term) list -> local_theory -> local_theory
-
-  val add_fixpat: Attrib.binding * string list -> theory -> theory
-  val add_fixpat_i: Thm.binding * term list -> theory -> theory
+  val add_fixpat: Thm.binding * term list -> theory -> theory
+  val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
   val add_matchers: (string * string) list -> theory -> theory
   val setup: theory -> theory
 end;
@@ -24,14 +19,6 @@
 structure FixrecPackage: FIXREC_PACKAGE =
 struct
 
-(* legacy type inference *)
-(* used by the domain package *)
-fun legacy_infer_term thy t =
-  singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
-
-fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
-
-
 val fix_eq2 = @{thm fix_eq2};
 val def_fix_ind = @{thm def_fix_ind};
 
@@ -341,20 +328,9 @@
 local
 (* code adapted from HOL/Tools/primrec_package.ML *)
 
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
-  let
-    val ((fixes, spec), _) = prep_spec
-      raw_fixes (map (single o apsnd single) raw_spec) ctxt
-  in (fixes, map (apsnd the_single) spec) end;
-
 fun gen_fixrec
   (set_group : bool)
-  (prep_spec : (binding * 'a option * mixfix) list ->
-       (Attrib.binding * 'b list) list list ->
-      Proof.context ->
-   (((binding * typ) * mixfix) list * (Attrib.binding * term list) list)
-    * Proof.context
-  )
+  prep_spec
   (strict : bool)
   raw_fixes
   raw_spec
@@ -362,7 +338,7 @@
   let
     val (fixes : ((binding * typ) * mixfix) list,
          spec : (Attrib.binding * term) list) =
-          prepare_spec prep_spec lthy raw_fixes raw_spec;
+          fst (prep_spec raw_fixes raw_spec lthy);
     val chead_of_spec =
       chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
     fun name_of (Free (n, _)) = n
@@ -405,8 +381,8 @@
 
 in
 
-val add_fixrec_i = gen_fixrec false Specification.check_specification;
-val add_fixrec = gen_fixrec true Specification.read_specification;
+val add_fixrec = gen_fixrec false Specification.check_spec;
+val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
 
 end; (* local *)
 
@@ -434,8 +410,8 @@
     (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   end;
 
-val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
-val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
+val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
+val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
 
 
 (*************************************************************************)
@@ -444,43 +420,14 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-(* bool parser *)
-val fixrec_strict = P.opt_keyword "permissive" >> not;
-
-fun pipe_error t = P.!!! (Scan.fail_with (K
-  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-(* (Attrib.binding * string) parser *)
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
-  ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-(* ((Attrib.binding * string) list) parser *)
-val statements = P.enum1 "|" statement;
-
-(* (((xstring option * bool) * (Binding.binding * string option * Mixfix.mixfix) list)
-   * (Attrib.binding * string) list) parser *)
-val fixrec_decl =
-  P.opt_target -- fixrec_strict -- P.fixes --| P.$$$ "where" -- statements;
+val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
+  ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
+    >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
 
-(* this builds a parser for a new keyword, fixrec, whose functionality 
-is defined by add_fixrec *)
-val _ =
-  let
-    val desc = "define recursive functions (HOLCF)";
-    fun fixrec (((opt_target, strict), raw_fixes), raw_spec) =
-      Toplevel.local_theory opt_target (add_fixrec strict raw_fixes raw_spec);
-  in
-    OuterSyntax.command "fixrec" desc K.thy_decl (fixrec_decl >> fixrec)
-  end;
-
-(* fixpat parser *)
-val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
-
-val _ =
-  OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
-    (fixpat_decl >> (Toplevel.theory o add_fixpat));
+val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
+  (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
   
-end; (* local structure *)
+end;
 
 val setup = FixrecMatchData.init;
 
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/args.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -227,7 +227,7 @@
 val bang_facts = Scan.peek (fn context =>
   P.position ($$$ "!") >> (fn (_, pos) =>
     (warning ("use of prems in proof method" ^ Position.str_of pos);
-      Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
+      Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
 
 val from_to =
   P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -185,9 +185,11 @@
 
 (* axioms and definitions *)
 
+val named_spec = SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
+
 val _ =
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
-    (Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
+    (Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms));
 
 val opt_unchecked_overloaded =
   Scan.optional (P.$$$ "(" |-- P.!!!
@@ -196,7 +198,7 @@
 
 val _ =
   OuterSyntax.command "defs" "define constants" K.thy_decl
-    (opt_unchecked_overloaded -- Scan.repeat1 SpecParse.spec_name
+    (opt_unchecked_overloaded -- Scan.repeat1 named_spec
       >> (Toplevel.theory o IsarCmd.add_defs));
 
 
@@ -254,7 +256,7 @@
 val _ =
   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
     (Scan.optional P.fixes [] --
-      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) []
+      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.specs)) []
     >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
 
 
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/local_defs.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -135,7 +135,7 @@
 fun export inner outer =    (*beware of closure sizes*)
   let
     val exp = Assumption.export false inner outer;
-    val prems = Assumption.prems_of inner;
+    val prems = Assumption.all_prems_of inner;
   in fn th =>
     let
       val th' = exp th;
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -301,7 +301,7 @@
   in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
 
 fun pretty_thm ctxt th =
-  let val asms = map Thm.term_of (Assumption.assms_of ctxt)
+  let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
   in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
 
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
@@ -1370,7 +1370,7 @@
           Pretty.commas (map prt_fix fixes))];
 
       (*prems*)
-      val prems = Assumption.prems_of ctxt;
+      val prems = Assumption.all_prems_of ctxt;
       val len = length prems;
       val suppressed = len - ! prems_limit;
       val prt_prems = if null prems then []
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/spec_parse.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -13,10 +13,10 @@
   val opt_attribs: Attrib.src list parser
   val thm_name: string -> Attrib.binding parser
   val opt_thm_name: string -> Attrib.binding parser
-  val spec: (Attrib.binding * string list) parser
-  val named_spec: (Attrib.binding * string list) parser
-  val spec_name: ((binding * string) * Attrib.src list) parser
-  val spec_opt_name: ((binding * string) * Attrib.src list) parser
+  val spec: (Attrib.binding * string) parser
+  val specs: (Attrib.binding * string list) parser
+  val alt_specs: (Attrib.binding * string) list parser
+  val where_alt_specs: (Attrib.binding * string) list parser
   val xthm: (Facts.ref * Attrib.src list) parser
   val xthms1: (Facts.ref * Attrib.src list) list parser
   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
@@ -30,8 +30,6 @@
   val statement: (Attrib.binding * (string * string list) list) list parser
   val general_statement: (Element.context list * Element.statement) parser
   val statement_keyword: string parser
-  val specification:
-    (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
 end;
 
 structure SpecParse: SPEC_PARSE =
@@ -54,11 +52,13 @@
   Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
     Attrib.empty_binding;
 
-val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
-val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
+val spec = opt_thm_name ":" -- P.prop;
+val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
 
-val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
-val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
+val alt_specs =
+  P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
+
+val where_alt_specs = P.where_ |-- P.!!! alt_specs;
 
 val xthm =
   P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
@@ -143,9 +143,4 @@
 
 val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
 
-
-(* specifications *)
-
-val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
-
 end;
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/specification.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -8,16 +8,22 @@
 signature SPECIFICATION =
 sig
   val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
+  val check_spec:
+    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+  val read_spec:
+    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+  val check_free_spec:
+    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+  val read_free_spec:
+    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   val check_specification: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term list) list list -> Proof.context ->
+    (Attrib.binding * term list) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val read_specification: (binding * string option * mixfix) list ->
-    (Attrib.binding * string list) list list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val check_free_specification: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term list) list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val read_free_specification: (binding * string option * mixfix) list ->
     (Attrib.binding * string list) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val axiomatization: (binding * typ option * mixfix) list ->
@@ -97,7 +103,7 @@
       in fold_rev close bounds A end;
   in map close_form As end;
 
-fun prep_spec prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
+fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
 
@@ -122,15 +128,30 @@
     val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
   in ((params, name_atts ~~ specs), specs_ctxt) end;
 
-fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src x;
-fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) x;
+
+fun single_spec (a, prop) = [(a, [prop])];
+fun the_spec (a, [prop]) = (a, prop);
+
+fun prep_spec prep_vars parse_prop prep_att do_close vars specs =
+  prepare prep_vars parse_prop prep_att do_close
+    vars (map single_spec specs) #>> apsnd (map the_spec);
+
+fun prep_specification prep_vars parse_prop prep_att vars specs =
+  prepare prep_vars parse_prop prep_att true [specs];
 
 in
 
-fun read_specification x = read_spec true x;
-fun check_specification x = check_spec true x;
-fun read_free_specification vars specs = read_spec false vars [specs];
-fun check_free_specification vars specs = check_spec false vars [specs];
+fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;
+fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true x;
+
+fun check_free_spec x = prep_spec ProofContext.cert_vars (K I) (K I) false x;
+fun read_free_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src false x;
+
+fun check_specification vars specs =
+  prepare ProofContext.cert_vars (K I) (K I) true vars [specs];
+
+fun read_specification vars specs =
+  prepare ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
 
 end;
 
@@ -139,7 +160,7 @@
 
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
-    val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
+    val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
     val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
 
     (*consts*)
@@ -147,12 +168,16 @@
     val subst = Term.subst_atomic (map Free xs ~~ consts);
 
     (*axioms*)
-    val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom  (* FIXME proper use of binding!? *)
-          ((map o apfst) Binding.name (PureThy.name_multi (Binding.name_of b) (map subst props)))
-        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
+    val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
+        fold_map Thm.add_axiom
+          (map (apfst (fn a => Binding.map_name (K a) b))
+            (PureThy.name_multi (Binding.name_of b) (map subst props)))
+        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
+
+    (*facts*)
     val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
       (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
+
     val _ =
       if not do_print then ()
       else print_consts (ProofContext.init thy') (K false) xs;
@@ -164,10 +189,9 @@
 
 (* definition *)
 
-fun gen_def do_print prep (raw_var, (raw_a, raw_prop)) lthy =
+fun gen_def do_print prep (raw_var, raw_spec) lthy =
   let
-    val (vars, [((raw_name, atts), [prop])]) =
-      fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
+    val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
     val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
     val var as (b, _) =
       (case vars of
@@ -193,16 +217,16 @@
       else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   in ((lhs, (def_name, th')), lthy3) end;
 
-val definition = gen_def false check_free_specification;
-val definition_cmd = gen_def true read_free_specification;
+val definition = gen_def false check_free_spec;
+val definition_cmd = gen_def true read_free_spec;
 
 
 (* abbreviation *)
 
 fun gen_abbrev do_print prep mode (raw_var, raw_prop) lthy =
   let
-    val ((vars, [(_, [prop])]), _) =
-      prep (the_list raw_var) [(("", []), [raw_prop])]
+    val ((vars, [(_, prop)]), _) =
+      prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
         (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
     val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
     val var =
@@ -223,8 +247,8 @@
     val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
   in lthy' end;
 
-val abbreviation = gen_abbrev false check_free_specification;
-val abbreviation_cmd = gen_abbrev true read_free_specification;
+val abbreviation = gen_abbrev false check_free_spec;
+val abbreviation_cmd = gen_abbrev true read_free_spec;
 
 
 (* notation *)
@@ -256,15 +280,12 @@
 
 local
 
-fun subtract_prems ctxt1 ctxt2 =
-  Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2);
-
 fun prep_statement prep_att prep_stmt elems concl ctxt =
   (case concl of
     Element.Shows shows =>
       let
         val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
-        val prems = subtract_prems ctxt elems_ctxt;
+        val prems = Assumption.local_prems_of elems_ctxt ctxt;
         val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
         val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
       in ((prems, stmt, []), goal_ctxt) end
@@ -300,7 +321,7 @@
 
         val atts = map (Attrib.internal o K)
           [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
-        val prems = subtract_prems ctxt elems_ctxt;
+        val prems = Assumption.local_prems_of elems_ctxt ctxt;
         val stmt = [((Binding.empty, atts), [(thesis, [])])];
 
         val (facts, goal_ctxt) = elems_ctxt
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/theory_target.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -52,7 +52,7 @@
     val fixes =
       map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
     val assumes =
-      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.assms_of ctxt);
+      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.all_assms_of ctxt);
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);
@@ -109,7 +109,7 @@
     val th = Goal.norm_result raw_th;
     val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
     val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
-    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
+    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
     val nprems = Thm.nprems_of th' - Thm.nprems_of th;
 
     (*export fixes*)
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Tools/find_theorems.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -336,7 +336,7 @@
 
 fun find_theorems ctxt opt_goal rem_dups raw_criteria =
   let
-    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1));
+    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.all_prems_of ctxt) 1));
     val opt_goal' = Option.map add_prems opt_goal;
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/assumption.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/assumption.ML
     Author:     Makarius
 
-Local assumptions, parameterized by export rules.
+Context assumptions, parameterized by export rules.
 *)
 
 signature ASSUMPTION =
@@ -10,12 +10,13 @@
   val assume_export: export
   val presume_export: export
   val assume: cterm -> thm
-  val assms_of: Proof.context -> cterm list
-  val prems_of: Proof.context -> thm list
+  val all_assms_of: Proof.context -> cterm list
+  val all_prems_of: Proof.context -> thm list
   val extra_hyps: Proof.context -> thm -> term list
+  val local_assms_of: Proof.context -> Proof.context -> cterm list
+  val local_prems_of: Proof.context -> Proof.context -> thm list
   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
   val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
-  val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
   val export: bool -> Proof.context -> Proof.context -> thm -> thm
   val export_term: Proof.context -> Proof.context -> term -> term
   val export_morphism: Proof.context -> Proof.context -> morphism
@@ -54,7 +55,7 @@
 (** local context data **)
 
 datatype data = Data of
- {assms: (export * cterm list) list,    (*assumes and views: A ==> _*)
+ {assms: (export * cterm list) list,    (*assumes: A ==> _*)
   prems: thm list};                     (*prems: A |- A*)
 
 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
@@ -68,18 +69,31 @@
 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
 
-val assumptions_of = #assms o rep_data;
-val assms_of = maps #2 o assumptions_of;
-val prems_of = #prems o rep_data;
+
+(* all assumptions *)
+
+val all_assumptions_of = #assms o rep_data;
+val all_assms_of = maps #2 o all_assumptions_of;
+val all_prems_of = #prems o rep_data;
 
-fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
+fun extra_hyps ctxt th =
+  subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
+
+(*named prems -- legacy feature*)
+val _ = Context.>>
+  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
+    fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
 
 
-(* named prems -- legacy feature *)
+(* local assumptions *)
+
+fun local_assumptions_of inner outer =
+  Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
 
-val _ = Context.>>
-  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
-    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
+val local_assms_of = maps #2 oo local_assumptions_of;
+
+fun local_prems_of inner outer =
+  Library.drop (length (all_prems_of outer), all_prems_of inner);
 
 
 (* add assumptions *)
@@ -92,27 +106,16 @@
 
 val add_assumes = add_assms assume_export;
 
-fun add_view outer view = map_data (fn (asms, prems) =>
-  let
-    val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
-    val asms' = asms1 @ [(assume_export, view)] @ asms2;
-  in (asms', prems) end);
-
 
 (* export *)
 
-fun diff_assms inner outer =
-  Library.drop (length (assumptions_of outer), assumptions_of inner);
-
 fun export is_goal inner outer =
-  let val asms = diff_assms inner outer in
-    MetaSimplifier.norm_hhf_protect
-    #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
-    #> MetaSimplifier.norm_hhf_protect
-  end;
+  MetaSimplifier.norm_hhf_protect #>
+  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
+  MetaSimplifier.norm_hhf_protect;
 
 fun export_term inner outer =
-  fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer);
+  fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
 
 fun export_morphism inner outer =
   let
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/goal.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -110,7 +110,7 @@
     val cert = Thm.cterm_of thy;
     val certT = Thm.ctyp_of thy;
 
-    val assms = Assumption.assms_of ctxt;
+    val assms = Assumption.all_assms_of ctxt;
     val As = map Thm.term_of assms;
 
     val xs = map Free (fold Term.add_frees (prop :: As) []);
diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Tools/quickcheck.ML	Thu Mar 12 22:16:25 2009 +0100
@@ -144,7 +144,7 @@
 fun test_goal_auto int state =
   let
     val ctxt = Proof.context_of state;
-    val assms = map term_of (Assumption.assms_of ctxt);
+    val assms = map term_of (Assumption.all_assms_of ctxt);
     val Test_Params { size, iterations, default_type } =
       (snd o Data.get o Proof.theory_of) state;
     fun test () =