--- 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
--- 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, ...}) =
--- 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