--- a/src/Pure/Isar/locale.ML Sat Jun 17 19:37:54 2006 +0200
+++ b/src/Pure/Isar/locale.ML Sat Jun 17 19:37:55 2006 +0200
@@ -513,7 +513,7 @@
(* parameter types *)
fun frozen_tvars ctxt Ts =
- #1 (Variable.monomorphic_inst (map Logic.mk_type Ts) ctxt)
+ #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
|> map (fn ((xi, S), T) => (xi, (S, T)));
fun unify_frozen ctxt maxidx Ts Us =
@@ -1794,8 +1794,8 @@
end;
val _ = Context.add_setup
- (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);
+ (add_locale_i true "var" empty [Fixes [(Term.internal "x", NONE, NoSyn)]] #> snd #>
+ add_locale_i true "struct" empty [Fixes [(Term.internal "S", NONE, Structure)]] #> snd);
@@ -1853,7 +1853,7 @@
elems_ctxt' |> mk_stmt (map (apsnd (K []) o fst) concl ~~ propp);
fun after_qed' results =
- let val loc_results = results |> (map o map)
+ let val loc_results = results |> map
(ProofContext.export_standard goal_ctxt loc_ctxt') in
curry (locale_results kind loc ((names ~~ loc_attss) ~~ loc_results)) loc_ctxt
#-> (fn res =>