Tuned signature of Locale.add_locale(_i).

--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 18 20:10:51 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 20 17:15:35 2006 +0100
@@ -342,7 +342,7 @@
     ((P.opt_keyword "open" >> not) -- P.name
         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
       >> (Toplevel.theory_context o (fn ((is_open, name), (expr, elems)) =>
-             Locale.add_locale is_open name expr elems #> (fn (_, ctxt, thy) => (ctxt, thy)))));
+             Locale.add_locale is_open name expr elems #> (fn ((_, ctxt), thy) => (ctxt, thy)))));
 
 val opt_inst =
   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];

--- a/src/Pure/Isar/locale.ML	Sat Mar 18 20:10:51 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 20 17:15:35 2006 +0100
@@ -72,9 +72,9 @@
   val print_local_registrations: bool -> string -> Proof.context -> unit
 
   val add_locale: bool -> bstring -> expr -> Element.context list -> theory
-    -> string * Proof.context (*body context!*) * theory
+    -> (string * Proof.context (*body context!*)) * theory
   val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory
-    -> string * Proof.context (*body context!*) * theory
+    -> (string * Proof.context (*body context!*)) * theory
 
   (* Storing results *)
   val note_thmss: string -> xstring ->
@@ -931,6 +931,45 @@
   | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
 
 
+(* experimental code for type inference *)
+
+local
+
+fun declare_int_elem (ctxt, Fixes fixes) =
+      (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
+        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
+  | declare_int_elem (ctxt, _) = (ctxt, []);
+
+fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
+      let val (vars, _) = prep_vars fixes ctxt
+      in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
+  | declare_ext_elem prep_vars (ctxt, Constrains csts) =
+      let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
+      in (ctxt', []) end
+  | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
+  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
+  | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
+
+fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
+    let val (ctxt', propps) =
+      (case elems of
+        Int es => foldl_map declare_int_elem (ctxt, es)
+      | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
+      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
+    in (ctxt', propps) end
+  | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
+
+in
+
+(* The Plan:
+- tell context about parameters and their syntax (possibly also types)
+- add declarations to context
+- retrieve parameter types
+*)
+
+end; (* local *)
+
+
 (* propositions and bindings *)
 
 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
@@ -1708,7 +1747,7 @@
         lparams = map #1 (params_of body_elemss),
         abbrevs = [],
         regs = []};
-  in (name, ProofContext.transfer thy' body_ctxt, thy') end;
+  in ((name, ProofContext.transfer thy' body_ctxt), thy') end;
 
 in
 
@@ -1718,8 +1757,8 @@
 end;
 
 val _ = Context.add_setup
- (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> #3 #>
-  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] #> #3);
+ (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> snd #>
+  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] #> snd);
 
 
 

--- a/src/Pure/Tools/class_package.ML	Sat Mar 18 20:10:51 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Mon Mar 20 17:15:35 2006 +0100
@@ -318,14 +318,14 @@
 fun add_locale opn name expr body thy =
   thy
   |> Locale.add_locale opn name expr body
-  |> (fn (_, ctxt, thy) => (ctxt, thy))
+  |> (fn ((_, ctxt), thy) => (ctxt, thy))
   ||>> `(fn thy => intro_incr thy name expr)
   |-> (fn (ctxt, intro) => pair ((Sign.full_name thy name, intro), ctxt));
 
 fun add_locale_i opn name expr body thy =
   thy
   |> Locale.add_locale_i opn name expr body
-  |> (fn (_, ctxt, thy) => (ctxt, thy))
+  |> (fn ((_, ctxt), thy) => (ctxt, thy))
   ||>> `(fn thy => intro_incr thy name expr)
   |-> (fn (ctxt, intro) => pair ((name, intro), ctxt));