merged

--- a/src/HOL/ex/ROOT.ML	Sat Jan 31 09:04:42 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Sun Feb 01 19:59:20 2009 +0100
@@ -3,6 +3,8 @@
 Miscellaneous examples for Higher-Order Logic.
 *)
 
+set Toplevel.timing;
+
 no_document use_thys [
   "State_Monad",
   "Efficient_Nat_examples",

--- a/src/Pure/Isar/class.ML	Sat Jan 31 09:04:42 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sun Feb 01 19:59:20 2009 +0100
@@ -128,12 +128,12 @@
       let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
 
     (* preproceesing elements, retrieving base sort from type-checked elements *)
+    val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
+      #> redeclare_operations thy sups
+      #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
+      #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
     val ((_, _, inferred_elems), _) = ProofContext.init thy
-      |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
-      |> redeclare_operations thy sups
-      |> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
-      |> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy))
-      |> prep_decl supexpr raw_elems;
+      |> prep_decl supexpr init_class_body raw_elems;
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
       | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
       | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
@@ -184,7 +184,7 @@
       (*#> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
           (K (TFree (Name.aT, base_sort))) supparams) FIXME really necessary?*)
             (*FIXME should constraints be issued in begin?*)
-      |> Expression.cert_declaration supexpr inferred_elems;
+      |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs = if null vs
       then error ("No type variable in part of specification element "
         ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))

--- a/src/Pure/Isar/expression.ML	Sat Jan 31 09:04:42 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Feb 01 19:59:20 2009 +0100
@@ -19,15 +19,15 @@
     Proof.context -> (term * term list) list list * Proof.context
 
   (* Declaring locales *)
-  val cert_declaration: expression_i -> Element.context_i list -> Proof.context ->
-    ((binding * typ option * mixfix) list * (string * morphism) list
+  val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
+    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
-  val cert_read_declaration: expression_i -> Element.context list -> Proof.context ->
-    ((binding * typ option * mixfix) list * (string * morphism) list
+  val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
+    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
       (*FIXME*)
-  val read_declaration: expression -> Element.context list -> Proof.context ->
-    ((binding * typ option * mixfix) list * (string * morphism) list
+  val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
+    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
   val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
     theory -> string * local_theory
@@ -351,7 +351,7 @@
 local
 
 fun prep_full_context_statement parse_typ parse_prop prep_vars_elem parse_inst prep_vars_inst prep_expr
-    strict do_close raw_import raw_elems raw_concl ctxt1 =
+    strict do_close raw_import init_body raw_elems raw_concl ctxt1 =
   let
     val thy = ProofContext.theory_of ctxt1;
 
@@ -388,20 +388,21 @@
     val fors = prep_vars_inst fixed ctxt1 |> fst;
     val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
     val (_, insts', ctxt3) = fold prep_inst raw_insts (0, [], ctxt2);
-    val (elems, ctxt4) = fold (prep_elem insts') raw_elems ([], ctxt3);
-    val (insts, elems', concl, ctxt5) =
-      prep_concl raw_concl (insts', elems, ctxt4);
+    val ctxt4 = init_body ctxt3;
+    val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
+    val (insts, elems', concl, ctxt6) =
+      prep_concl raw_concl (insts', elems, ctxt5);
 
     (* Retrieve parameter types *)
     val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes)
       | _ => fn ps => ps) (Fixes fors :: elems') [];
-    val (Ts, ctxt6) = fold_map ProofContext.inferred_param xs ctxt5; 
+    val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; 
     val parms = xs ~~ Ts;  (* params from expression and elements *)
 
     val Fixes fors' = finish_primitive parms I (Fixes fors);
     val (deps, elems'') = finish ctxt6 parms do_close insts elems';
 
-  in ((fors', deps, elems'', concl), (parms, ctxt6)) end
+  in ((fors', deps, elems'', concl), (parms, ctxt7)) end
 
 in
 
@@ -425,7 +426,7 @@
 fun prep_statement prep activate raw_elems raw_concl context =
   let
      val ((_, _, elems, concl), _) =
-       prep true false ([], []) raw_elems raw_concl context;
+       prep true false ([], []) I raw_elems raw_concl context;
      val (_, context') = context |>
        ProofContext.set_stmt true |>
        activate elems;
@@ -443,10 +444,10 @@
 
 local
 
-fun prep_declaration prep activate raw_import raw_elems context =
+fun prep_declaration prep activate raw_import init_body raw_elems context =
   let
     val ((fixed, deps, elems, _), (parms, ctxt')) =
-      prep false true raw_import raw_elems [] context ;
+      prep false true raw_import init_body raw_elems [] context ;
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
@@ -481,7 +482,7 @@
     val thy = ProofContext.theory_of context;
 
     val ((fixed, deps, _, _), _) =
-      prep true true expression [] [] context;
+      prep true true expression I [] [] context;
     (* proof obligations *)
     val propss = map (props_of thy) deps;
 
@@ -732,7 +733,7 @@
       error ("Duplicate definition of locale " ^ quote name);
 
     val ((fixed, deps, body_elems), (parms, ctxt')) =
-      prep_decl raw_imprt raw_body (ProofContext.init thy);
+      prep_decl raw_imprt I raw_body (ProofContext.init thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
     val predicate_bname = if raw_predicate_bname = "" then bname