# HG changeset patch
# User wenzelm
# Date 1122556805 -7200
# Node ID 3aef68881781350a634b2f59e65e0f070cb2caf1
# Parent  c6a90f04924ec443c9e9342b6fd4d9b4281fabbb
Sign.typ_unify;
tuned;

diff -r c6a90f04924e -r 3aef68881781 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jul 28 15:20:04 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jul 28 15:20:05 2005 +0200
@@ -452,7 +452,7 @@
 
 fun unifyT ctxt (T, U) =
   let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
-  in #1 (Type.unify (Sign.tsig_of (theory_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
+  in #1 (Sign.typ_unify (theory_of ctxt) (T, U) (Vartab.empty, maxidx)) end;
 
 fun norm_term ctxt schematic =
   let
@@ -684,11 +684,11 @@
     val fixes = fixed_names_of inner \\ fixed_names_of outer;
     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
-  in fn thm => thm
-    |> Tactic.norm_hhf_rule
-    |> Seq.EVERY (rev exp_asms)
-    |> Seq.map (Drule.implies_intr_list view)
-    |> Seq.map (fn rule =>
+  in
+    Tactic.norm_hhf_rule
+    #> Seq.EVERY (rev exp_asms)
+    #> Seq.map (Drule.implies_intr_list view)
+    #> Seq.map (fn rule =>
       let
         val {thy, prop, ...} = Thm.rep_thm rule;
         val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes);
@@ -706,11 +706,11 @@
   let
     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
-  in fn thm =>thm
-    |> Tactic.norm_hhf_plain
-    |> Seq.EVERY (rev exp_asms)
-    |> Seq.map (Drule.implies_intr_list view)
-    |> Seq.map Tactic.norm_hhf_plain
+  in
+    Tactic.norm_hhf_plain
+    #> Seq.EVERY (rev exp_asms)
+    #> Seq.map (Drule.implies_intr_list view)
+    #> Seq.map Tactic.norm_hhf_plain
   end;
 
 val export = export_view [];
@@ -779,7 +779,8 @@
         val _ =    (*may not assign variables from text*)
           if null (map #1 (Envir.alist_of env) inter (map #1 (Drule.vars_of_terms (map #2 pairs))))
           then () else fail ();
-        fun norm_bind (xi, (_, t)) = if xi mem domain then SOME (xi, Envir.norm_term env t) else NONE;
+        fun norm_bind (xi, (_, t)) =
+          if mem_ix (xi, domain) then SOME (xi, Envir.norm_term env t) else NONE;
       in List.mapPartial norm_bind (Envir.alist_of env) end;