# HG changeset patch
# User wenzelm
# Date 1150565875 -7200
# Node ID fde2b5c0b42b03e302f196ca71c1c095e761b7b1
# Parent  3f844845ecb890ddd9e6a7b9537d7c628261ec35
Variable.importT_inst;
Term.internal;

diff -r 3f844845ecb8 -r fde2b5c0b42b src/Pure/Isar/locale.ML
--- 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 =>