# HG changeset patch
# User haftmann
# Date 1222063227 -7200
# Node ID e7adede08de56b803981234bc6ebcf5756ca2c6d
# Parent  c24bc53c815c0699c9cbe8c4b7bb670c5f6ba814
corrected sort intersection

diff -r c24bc53c815c -r e7adede08de5 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Mon Sep 22 08:00:26 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Mon Sep 22 08:00:27 2008 +0200
@@ -85,8 +85,10 @@
   let
     val thy = Thm.theory_of_thm thm;
     val tvars = (Term.add_tvars o Thm.prop_of) thm [];
-    fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v
-     of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort)))
+    val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
+    fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
+     of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar)
+          (tvar, (v, inter_sort (sort, sort'))))
       | NONE => NONE;
     val insts = map_filter mk_inst tvars;
   in Thm.instantiate (insts, []) thm end;
@@ -154,7 +156,7 @@
 fun norm_args thms =
   let
     val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
-    val k = fold (curry Int.max o num_args_of o Thm.plain_prop_of) thms 0;
+    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
   in
     thms
     |> map (expand_eta k)