# HG changeset patch
# User wenzelm
# Date 1274989062 -7200
# Node ID c96e119b7fe963c7f64d0754b5008d5c32c7435c
# Parent  86872cbae9e9217a3e33e60542afd949f00075d1# Parent  edfbd2a8234f6dd1a3e2af0b96c8c987f563e506
merged

diff -r 86872cbae9e9 -r c96e119b7fe9 NEWS
--- a/NEWS	Thu May 27 18:16:54 2010 +0200
+++ b/NEWS	Thu May 27 21:37:42 2010 +0200
@@ -504,6 +504,8 @@
   OuterParse    ~>  Parse
   OuterSyntax   ~>  Outer_Syntax
   SpecParse     ~>  Parse_Spec
+  TypeInfer     ~>  Type_Infer
+  PrintMode     ~>  Print_Mode
 
 Note that "open Legacy" simplifies porting of sources, but forgetting
 to remove it again will complicate porting again in the future.
diff -r 86872cbae9e9 -r c96e119b7fe9 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 18:16:54 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 21:37:42 2010 +0200
@@ -148,7 +148,7 @@
 ML {*
   fun check_syntax ctxt thm expected =
     let
-      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
+      val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm;
     in
       if obtained <> expected
       then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu May 27 21:37:42 2010 +0200
@@ -200,7 +200,7 @@
                            handle TERM _ => ct)
     in
         quote (
-        PrintMode.setmp [] (
+        Print_Mode.setmp [] (
         setmp_CRITICAL show_brackets false (
         setmp_CRITICAL show_all_types true (
         setmp_CRITICAL Syntax.ambiguity_is_error false (
@@ -229,7 +229,7 @@
                 val str =
                   setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
                 val u = Syntax.parse_term ctxt str
-                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
+                  |> Type_Infer.constrain T |> Syntax.check_term ctxt
             in
                 if match u
                 then quote str
@@ -239,14 +239,14 @@
               | SMART_STRING =>
                   error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
     in
-      PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
+      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
     end
     handle ERROR mesg => simple_smart_string_of_cterm ct
 
 val smart_string_of_thm = smart_string_of_cterm o cprop_of
 
-fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
-fun prin t = writeln (PrintMode.setmp []
+fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
+fun prin t = writeln (Print_Mode.setmp []
   (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
 fun pth (HOLThm(ren,thm)) =
     let
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu May 27 21:37:42 2010 +0200
@@ -56,7 +56,7 @@
 (*Prints an exception, then fails*)
 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
 
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
+val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
 
 fun mk_meta_eq th =
     (case concl_of th of
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu May 27 21:37:42 2010 +0200
@@ -32,7 +32,7 @@
 oracle mc_eindhoven_oracle =
 {*
 let
-  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
+  val eindhoven_term = Print_Mode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
 
   fun call_mc s =
     let
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 21:37:42 2010 +0200
@@ -487,7 +487,7 @@
         make_string sign (trm::list) =
            Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list
 in
-  PrintMode.setmp ["Mucke"] (make_string sign) terms
+  Print_Mode.setmp ["Mucke"] (make_string sign) terms
 end;
 
 fun callmc s =
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu May 27 21:37:42 2010 +0200
@@ -439,7 +439,7 @@
 
    fun string_of_typ T =
       setmp_CRITICAL show_sorts true
-       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
+       (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
    val fixestate = (case state_type of
          NONE => []
        | SOME s =>
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Thu May 27 21:37:42 2010 +0200
@@ -149,7 +149,7 @@
   end
 
 val add_function =
-  gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+  gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
 val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
 
 fun gen_function is_external prep default_constraint fixspec eqns config lthy =
@@ -163,7 +163,7 @@
   end
 
 val function =
-  gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+  gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
 val function_cmd = gen_function true Specification.read_spec "_::type"
 
 fun prepare_termination_proof prep_term raw_term_opt lthy =
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Thu May 27 21:37:42 2010 +0200
@@ -879,7 +879,7 @@
     val ranT = range_type fT
 
     val default = Syntax.parse_term lthy default_str
-      |> TypeInfer.constrain fT |> Syntax.check_term lthy
+      |> Type_Infer.constrain fT |> Syntax.check_term lthy
 
     val (globals, ctxt') = fix_globals domT ranT fvar lthy
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 27 21:37:42 2010 +0200
@@ -483,7 +483,7 @@
         val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
         val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
-                      PrintMode.setmp [] multiline_string_for_scope scope
+                      Print_Mode.setmp [] multiline_string_for_scope scope
         val kodkod_sat_solver =
           Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
         val bit_width = if bits = 0 then 16 else bits + 1
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 21:37:42 2010 +0200
@@ -3306,7 +3306,7 @@
              Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
              @ maps pretty_entry xs
           end
-    val p = PrintMode.with_modes print_modes (fn () =>
+    val p = Print_Mode.with_modes print_modes (fn () =>
       Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
         @ pretty_stat)) ();
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 21:37:42 2010 +0200
@@ -254,7 +254,7 @@
             SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
           | NONE =>
             (* Variable from the ATP, say "X1" *)
-            TypeInfer.param 0 (a, HOLogic.typeS)
+            Type_Infer.param 0 (a, HOLogic.typeS)
     end
 
 (*Invert the table of translations between Isabelle and ATPs*)
@@ -453,7 +453,7 @@
     val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
   in repair_tvar_sorts vt t end
 fun check_formula ctxt =
-  TypeInfer.constrain @{typ bool}
+  Type_Infer.constrain @{typ bool}
   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
 
 
@@ -911,7 +911,7 @@
 fun string_for_proof ctxt i n =
   let
     fun fix_print_mode f =
-      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                       (print_mode_value ())) f
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu May 27 21:37:42 2010 +0200
@@ -138,7 +138,7 @@
 (* HOL syntax *)
 
 val typeS: sort = ["HOL.type"];
-val typeT = TypeInfer.anyT typeS;
+val typeT = Type_Infer.anyT typeS;
 
 
 (* bool and set *)
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Thu May 27 21:37:42 2010 +0200
@@ -197,7 +197,7 @@
     val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
       (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
     val rhs = singleton (Syntax.check_terms ctxt)
-      (TypeInfer.constrain varT raw_rhs);
+      (Type_Infer.constrain varT raw_rhs);
   in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
 
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOLCF/IOA/meta_theory/automaton.ML
--- a/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 27 21:37:42 2010 +0200
@@ -18,8 +18,8 @@
 structure Automaton: AUTOMATON =
 struct
 
-val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
-val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
+val string_of_typ = Print_Mode.setmp [] o Syntax.string_of_typ_global;
+val string_of_term = Print_Mode.setmp [] o Syntax.string_of_term_global;
 
 exception malformed;
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 27 21:37:42 2010 +0200
@@ -185,7 +185,7 @@
 fun mk_lam  (x,T) = Abs(x,dummyT,T);
 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
 end
 
 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
diff -r 86872cbae9e9 -r c96e119b7fe9 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu May 27 21:37:42 2010 +0200
@@ -463,7 +463,7 @@
 
   fun legacy_infer_term thy t =
       singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
-  fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+  fun legacy_infer_prop thy t = legacy_infer_term thy (Type_Infer.constrain propT t);
   fun infer_props thy = map (apsnd (legacy_infer_prop thy));
   fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
   fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/General/print_mode.ML	Thu May 27 21:37:42 2010 +0200
@@ -22,7 +22,7 @@
   val closure: ('a -> 'b) -> 'a -> 'b
 end;
 
-structure PrintMode: PRINT_MODE =
+structure Print_Mode: PRINT_MODE =
 struct
 
 val input = "input";
@@ -49,5 +49,5 @@
 
 end;
 
-structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
-open BasicPrintMode;
+structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
+open Basic_Print_Mode;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Thu May 27 21:37:42 2010 +0200
@@ -275,7 +275,7 @@
      of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
          of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
              of SOME (_, ty' as TVar (vi, sort)) =>
-                  if TypeInfer.is_param vi
+                  if Type_Infer.is_param vi
                     andalso Sorts.sort_le algebra (base_sort, sort)
                       then SOME (ty', TFree (Name.aT, base_sort))
                       else NONE
@@ -355,7 +355,7 @@
     |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
-    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
+    |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
   end;
 
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 27 21:37:42 2010 +0200
@@ -162,9 +162,9 @@
     val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
 
     (* type inference and contexts *)
-    val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
+    val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
-    val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
+    val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
     val res = Syntax.check_terms ctxt arg;
     val ctxt' = ctxt |> fold Variable.auto_fixes res;
 
@@ -345,9 +345,9 @@
       let
         val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
         val inst' = prep_inst ctxt parm_names inst;
-        val parm_types' = map (TypeInfer.paramify_vars o
+        val parm_types' = map (Type_Infer.paramify_vars o
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
-        val inst'' = map2 TypeInfer.constrain parm_types' inst';
+        val inst'' = map2 Type_Infer.constrain parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
         val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu May 27 21:37:42 2010 +0200
@@ -281,7 +281,7 @@
 
 fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
   (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
-    PrintMode.with_modes modes (Toplevel.print_state true) state));
+    Print_Mode.with_modes modes (Toplevel.print_state true) state));
 
 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
@@ -488,7 +488,7 @@
   in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
 
 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
-  PrintMode.with_modes modes (fn () =>
+  Print_Mode.with_modes modes (fn () =>
     writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
 
 in
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Thu May 27 21:37:42 2010 +0200
@@ -111,20 +111,20 @@
 
 (* states *)
 
-val empty_state = Future.value (SOME Toplevel.toplevel);
+val empty_state = Lazy.value (SOME Toplevel.toplevel);
 
 local
-
-val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]);
-
+  val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]);
 in
 
 fun define_state (id: state_id) =
-  Unsynchronized.change global_states (Symtab.update_new (id, empty_state))
-    handle Symtab.DUP dup => err_dup "state" dup;
+  NAMED_CRITICAL "Isar" (fn () =>
+    Unsynchronized.change global_states (Symtab.update_new (id, empty_state))
+      handle Symtab.DUP dup => err_dup "state" dup);
 
 fun put_state (id: state_id) state =
-  Unsynchronized.change global_states (Symtab.update (id, state));
+  NAMED_CRITICAL "Isar" (fn () =>
+    Unsynchronized.change global_states (Symtab.update (id, state)));
 
 fun the_state (id: state_id) =
   (case Symtab.lookup (! global_states) id of
@@ -137,9 +137,7 @@
 (* commands *)
 
 local
-
-val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
-
+  val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
 in
 
 fun define_command id tr =
@@ -158,9 +156,7 @@
 (* documents *)
 
 local
-
-val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
-
+  val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
 in
 
 fun define_document (id: document_id) document =
@@ -176,6 +172,18 @@
 end;
 
 
+(* execution *)
+
+local
+  val execution = Unsynchronized.ref (Future.value ());
+in
+
+fun execute e =
+  NAMED_CRITICAL "Isar" (fn () => (Future.cancel (! execution); execution := Future.fork e));
+
+end;
+
+
 
 (** main operations **)
 
@@ -196,9 +204,9 @@
       val end_state =
         the_state (the (#state (#3 (the
           (first_entry (fn (_, {next, ...}) => is_none next) document)))));
-      val _ =
-        Future.fork_deps [end_state] (fn () =>
-          (case Future.join end_state of
+      val _ =  (* FIXME regular execution (??) *)
+        Future.fork (fn () =>
+          (case Lazy.force end_state of
             SOME st =>
              (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
               ThyInfo.touch_child_thys name;
@@ -225,11 +233,11 @@
       let
         val state = the_state state_id;
         val state' =
-          Future.fork_deps [state] (fn () =>
-            (case Future.join state of
+          Lazy.lazy (fn () =>
+            (case Lazy.force state of
               NONE => NONE
             | SOME st => Toplevel.run_command name tr st));
-      in put_state state_id' state' end;
+      in put_state state_id' state'; state' end;
   in (state_id', ((id, state_id'), make_state') :: updates) end;
 
 fun report_updates updates =
@@ -246,19 +254,11 @@
       val new_document as Document {entries = new_entries, ...} = old_document
         |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
 
-      fun cancel_old id = fold_entries id
-        (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
-        old_document ();
-
       val (updates, new_document') =
         (case first_entry (is_changed old_entries) new_document of
-          NONE =>
-            (case first_entry (is_changed new_entries) old_document of
-              NONE => ([], new_document)
-            | SOME (_, id, _) => (cancel_old id; ([], new_document)))
+          NONE => ([], new_document)
         | SOME (prev, id, _) =>
             let
-              val _ = cancel_old id;
               val prev_state_id = the (#state (the_entry new_entries (the prev)));
               val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
               val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
@@ -266,7 +266,8 @@
 
       val _ = define_document new_id new_document';
       val _ = report_updates (map #1 updates);
-      val _ = List.app (fn (_, run) => run ()) updates;
+      val execs = map (fn (_, make) => make ()) updates;
+      val _ = execute (fn () => List.app (ignore o Lazy.force) execs);
     in () end);
 
 end;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 27 21:37:42 2010 +0200
@@ -577,7 +577,7 @@
       pattern orelse schematic orelse
         T |> Term.exists_subtype
           (fn TVar (xi, _) =>
-            not (TypeInfer.is_param xi) andalso
+            not (Type_Infer.is_param xi) andalso
               error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
           | _ => false)
   in T end;
@@ -599,7 +599,7 @@
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
-    TypeInfer.fixate_params (Variable.names_of ctxt) #>
+    Type_Infer.fixate_params (Variable.names_of ctxt) #>
     pattern ? Variable.polymorphic ctxt #>
     (map o Term.map_types) (prepare_patternT ctxt) #>
     (if pattern then prepare_dummies else map (check_dummies ctxt))
@@ -699,7 +699,7 @@
   in Variable.def_type ctxt pattern end;
 
 fun standard_infer_types ctxt ts =
-  TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
+  Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
     (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
     (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
   handle TYPE (msg, _, _) => error msg;
@@ -754,11 +754,11 @@
   let
     val {get_sort, map_const, map_free} = term_context ctxt;
 
-    val (T', _) = TypeInfer.paramify_dummies T 0;
+    val (T', _) = Type_Infer.paramify_dummies T 0;
     val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
     val (syms, pos) = Syntax.parse_token markup text;
 
-    fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
+    fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
       handle ERROR msg => SOME msg;
     val t =
       Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
@@ -883,7 +883,7 @@
 in
 
 fun read_terms ctxt T =
-  map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
+  map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
 
 val match_bind = gen_bind read_terms;
 val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Thu May 27 21:37:42 2010 +0200
@@ -82,7 +82,7 @@
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     val ts = map2 parse Ts ss;
     val ts' =
-      map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
+      map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
       |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
       |> Variable.polymorphic ctxt;
     val Ts' = map Term.fastype_of ts';
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Thu May 27 21:37:42 2010 +0200
@@ -96,13 +96,13 @@
       (case duplicates (op =) commons of [] => ()
       | dups => error ("Duplicate local variables " ^ commas_quote dups));
     val frees = rev ((fold o fold_aterms) add_free As (rev commons));
-    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
+    val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
     val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
 
     fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
       | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
       | abs_body lev y (t as Free (x, T)) =
-          if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
+          if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
           else t
       | abs_body _ _ a = a;
     fun close (y, U) B =
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Thu May 27 21:37:42 2010 +0200
@@ -200,8 +200,8 @@
   in
     not (is_class andalso (same_shape orelse class_global)) ?
       (Context.mapping_result
-        (Sign.add_abbrev PrintMode.internal arg)
-        (ProofContext.add_abbrev PrintMode.internal arg)
+        (Sign.add_abbrev Print_Mode.internal arg)
+        (ProofContext.add_abbrev Print_Mode.internal arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           same_shape ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
@@ -225,7 +225,7 @@
   in
     lthy |>
      (if is_locale then
-        Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
+        Local_Theory.theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in
             syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
@@ -235,7 +235,7 @@
         Local_Theory.theory
           (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
-    |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
+    |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
     |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
   end;
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Thu May 27 21:37:42 2010 +0200
@@ -99,6 +99,11 @@
                       case _ => state
                     }
                   }
+                  else if (kind == Markup.FACT_DECL || kind == Markup.LOCAL_FACT_DECL ||
+                      kind == Markup.ATTRIBUTE || kind == Markup.FIXED_DECL) {
+                    // FIXME usually displaced due to lack of full history support
+                    state
+                  }
                   else {
                     state.add_markup(
                       command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Thu May 27 21:37:42 2010 +0200
@@ -212,7 +212,7 @@
   in
     fn ty => fn s =>
       (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
-      |> TypeInfer.constrain ty |> Syntax.check_term ctxt
+      |> Type_Infer.constrain ty |> Syntax.check_term ctxt
   end;
 
 fun read_proof thy =
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu May 27 21:37:42 2010 +0200
@@ -93,7 +93,7 @@
   let
     val kind = ThySyntax.span_kind span;
     val toks = ThySyntax.span_content span;
-    val text = implode (map (PrintMode.setmp [] ThySyntax.present_token) toks);
+    val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
   in
     (case kind of
       ThySyntax.Command name => parse_command name text
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/ROOT.ML	Thu May 27 21:37:42 2010 +0200
@@ -309,6 +309,8 @@
 structure OuterParse = Parse;
 structure OuterSyntax = Outer_Syntax;
 structure SpecParse = Parse_Spec;
+structure TypeInfer = Type_Infer;
+structure PrintMode = Print_Mode;
 
 end;
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu May 27 21:37:42 2010 +0200
@@ -259,7 +259,7 @@
 
 type mode = string * bool;
 val mode_default = ("", true);
-val mode_input = (PrintMode.input, true);
+val mode_input = (Print_Mode.input, true);
 
 
 (* empty_syntax *)
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Thy/html.ML	Thu May 27 21:37:42 2010 +0200
@@ -42,7 +42,7 @@
 (* mode *)
 
 val htmlN = "HTML";
-fun html_mode f x = PrintMode.with_modes [htmlN] f x;
+fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
 
 
 (* common markup *)
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu May 27 21:37:42 2010 +0200
@@ -153,7 +153,7 @@
       | expand (Antiquote.Antiq (ss, (pos, _))) =
           let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
             options opts (fn () => command src state) ();  (*preview errors!*)
-            PrintMode.with_modes (! modes @ Latex.modes)
+            Print_Mode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
           end
       | expand (Antiquote.Open _) = ""
@@ -429,7 +429,7 @@
   ("display", setmp_CRITICAL display o boolean),
   ("break", setmp_CRITICAL break o boolean),
   ("quotes", setmp_CRITICAL quotes o boolean),
-  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
+  ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
   ("margin", setmp_CRITICAL Pretty.margin_default o integer),
   ("indent", setmp_CRITICAL indent o integer),
   ("source", setmp_CRITICAL source o boolean),
@@ -455,7 +455,7 @@
 
 fun pretty_term_typ ctxt (style, t) =
   let val t' = style t
-  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
+  in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
 
 fun pretty_term_typeof ctxt (style, t) =
   Syntax.pretty_typ ctxt (Term.fastype_of (style t));
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/codegen.ML	Thu May 27 21:37:42 2010 +0200
@@ -109,9 +109,9 @@
 
 val margin = Unsynchronized.ref 80;
 
-fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
+fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
 
-val str = PrintMode.setmp [] Pretty.str;
+val str = Print_Mode.setmp [] Pretty.str;
 
 (**** Mixfix syntax ****)
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/consts.ML	Thu May 27 21:37:42 2010 +0200
@@ -270,7 +270,7 @@
   let
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
-    val force_expand = mode = PrintMode.internal;
+    val force_expand = mode = Print_Mode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
       error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/old_goals.ML	Thu May 27 21:37:42 2010 +0200
@@ -223,7 +223,7 @@
       |> ProofContext.allow_dummies
       |> ProofContext.set_mode ProofContext.mode_schematic;
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
-  in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
+  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
 
 fun read_term thy = simple_read_term thy dummyT;
 fun read_prop thy = simple_read_term thy propT;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/sign.ML	Thu May 27 21:37:42 2010 +0200
@@ -271,7 +271,7 @@
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
         val msg = cat_lines
-          (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
+          (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/type_infer.ML	Thu May 27 21:37:42 2010 +0200
@@ -20,7 +20,7 @@
     term list -> term list
 end;
 
-structure TypeInfer: TYPE_INFER =
+structure Type_Infer: TYPE_INFER =
 struct
 
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/variable.ML	Thu May 27 21:37:42 2010 +0200
@@ -168,7 +168,7 @@
     (case Vartab.lookup types xi of
       NONE =>
         if pattern then NONE
-        else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
+        else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
     | some => some)
   end;
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu May 27 21:37:42 2010 +0200
@@ -105,19 +105,19 @@
 infixr 5 @|;
 fun x @@ y = [x, y];
 fun xs @| y = xs @ [y];
-val str = PrintMode.setmp [] Pretty.str;
+val str = Print_Mode.setmp [] Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
-fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r);
+fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
 val brackets = enclose "(" ")" o Pretty.breaks;
-fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r);
+fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
 fun enum_default default sep l r [] = str default
   | enum_default default sep l r xs = enum sep l r xs;
 fun semicolon ps = Pretty.block [concat ps, str ";"];
 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
-fun indent i = PrintMode.setmp [] (Pretty.indent i);
+fun indent i = Print_Mode.setmp [] (Pretty.indent i);
 
-fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
-fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
+fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
+fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p);
 
 
 (** names and variable name contexts **)
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Tools/WWW_Find/html_unicode.ML
--- a/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 21:37:42 2010 +0200
@@ -19,7 +19,7 @@
 (* mode *)
 
 val htmlunicodeN = "HTMLUnicode";
-fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
+fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
 
 (* symbol output *)
 
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/nbe.ML	Thu May 27 21:37:42 2010 +0200
@@ -506,7 +506,7 @@
             val ts' = take_until is_dict ts;
             val c = const_of_idx idx;
             val T = map_type_tvar (fn ((v, i), _) =>
-              TypeInfer.param typidx (v ^ string_of_int i, []))
+              Type_Infer.param typidx (v ^ string_of_int i, []))
                 (Sign.the_const_type thy c);
             val typidx' = typidx + 1;
           in of_apps bounds (Term.Const (c, T), ts') typidx' end
@@ -548,9 +548,9 @@
   let
     val ty' = typ_of_itype program vs0 ty;
     fun type_infer t =
-      singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
+      singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
         (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
-      (TypeInfer.constrain ty' t);
+      (Type_Infer.constrain ty' t);
     fun check_tvars t = if null (Term.add_tvars t []) then t else
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
@@ -620,7 +620,7 @@
     val t' = norm thy t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
+    val p = Print_Mode.with_modes modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/Tools/value.ML
--- a/src/Tools/value.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/value.ML	Thu May 27 21:37:42 2010 +0200
@@ -47,7 +47,7 @@
       | SOME name => value_select name ctxt t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
+    val p = Print_Mode.with_modes modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Thu May 27 21:37:42 2010 +0200
@@ -403,7 +403,7 @@
   let
     val ctxt = ProofContext.init_global thy;
     fun read_is strs =
-      map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
+      map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
       |> Syntax.check_terms ctxt;
 
     val rec_tms = read_is srec_tms;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu May 27 21:37:42 2010 +0200
@@ -555,7 +555,7 @@
     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = ProofContext.init_global thy;
-    val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
+    val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
       #> Syntax.check_terms ctxt;
 
     val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
diff -r 86872cbae9e9 -r c96e119b7fe9 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Thu May 27 18:16:54 2010 +0200
+++ b/src/ZF/ind_syntax.ML	Thu May 27 21:37:42 2010 +0200
@@ -66,7 +66,7 @@
 
 (*read a constructor specification*)
 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
-    let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
+    let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> iT