# HG changeset patch
# User wenzelm
# Date 1333453635 -7200
# Node ID 323b7d74b2a83768362ab0bc6ca891c751e67f25
# Parent  b79bf8288b298f06a61c38285d63007fa03206e5
tuned;

diff -r b79bf8288b29 -r 323b7d74b2a8 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Apr 03 11:28:21 2012 +0200
+++ b/src/Pure/Isar/class.ML	Tue Apr 03 13:47:15 2012 +0200
@@ -486,13 +486,12 @@
   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
 
-fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
   (case instantiation_param lthy b of
     SOME c =>
       if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
       else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
-  | NONE => lthy |>
-      Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
+  | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
   let
diff -r b79bf8288b29 -r 323b7d74b2a8 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Apr 03 11:28:21 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 13:47:15 2012 +0200
@@ -69,16 +69,15 @@
 
 (* define *)
 
-fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params =
+  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
-fun class_foundation (ta as Target {target, ...})
-    (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params =
+  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
-    #> Class.const target ((b, mx), (type_params, lhs))
+    #> Class.const target ((b, mx), (#1 params, lhs))
     #> pair (lhs, def));
 
 fun target_foundation (ta as Target {is_locale, is_class, ...}) =
diff -r b79bf8288b29 -r 323b7d74b2a8 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Tue Apr 03 11:28:21 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Tue Apr 03 13:47:15 2012 +0200
@@ -158,14 +158,13 @@
   ##> Local_Theory.map_contexts (K synchronize_syntax)
   #-> (fn (_, def) => pair (Const (c, U), def));
 
-fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
   (case operation lthy b of
     SOME (c, (v, checked)) =>
       if mx <> NoSyn
       then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
       else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
-  | NONE => lthy
-      |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
+  | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
   let