src/Pure/thm.ML

--- a/src/Pure/thm.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/thm.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -47,8 +47,10 @@
   val lambda: cterm -> cterm -> cterm
   val adjust_maxidx_cterm: int -> cterm -> cterm
   val incr_indexes_cterm: int -> cterm -> cterm
-  val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
-  val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
+  val match: cterm * cterm ->
+    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
+  val first_order_match: cterm * cterm ->
+    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   (*theorems*)
   val rep_thm: thm ->
    {thy: theory,
@@ -120,8 +122,10 @@
   val equal_elim: thm -> thm -> thm
   val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
   val generalize: string list * string list -> int -> thm -> thm
-  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
-  val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
+  val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
+    thm -> thm
+  val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
+    cterm -> cterm
   val trivial: cterm -> thm
   val of_class: ctyp * class -> thm
   val strip_shyps: thm -> thm
@@ -312,12 +316,10 @@
     val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
     val sorts = Sorts.union sorts1 sorts2;
     fun mk_cTinst ((a, i), (S, T)) =
-      (Ctyp {T = TVar ((a, i), S), thy = thy, maxidx = i, sorts = sorts},
-       Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts});
-    fun mk_ctinst ((x, i), (T, t)) =
-      let val T = Envir.subst_type Tinsts T in
-        (Cterm {t = Var ((x, i), T), T = T, thy = thy, maxidx = i, sorts = sorts},
-         Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts})
+      (((a, i), S), Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts});
+    fun mk_ctinst ((x, i), (U, t)) =
+      let val T = Envir.subst_type Tinsts U in
+        (((x, i), T), Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts})
       end;
   in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;
 
@@ -1091,37 +1093,28 @@
 fun pretty_typing thy t T = Pretty.block
   [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T];
 
-fun add_inst (ct, cu) (thy, sorts) =
+fun add_inst (v as (_, T), cu) (thy, sorts) =
   let
-    val Cterm {t = t, T = T, ...} = ct;
-    val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
-    val thy' = Theory.merge (thy, merge_thys0 ct cu);
+    val Cterm {t = u, T = U, thy = thy2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
+    val thy' = Theory.merge (thy, thy2);
     val sorts' = Sorts.union sorts_u sorts;
   in
-    (case t of Var v =>
-      if T = U then ((v, (u, maxidx_u)), (thy', sorts'))
-      else raise TYPE (Pretty.string_of (Pretty.block
+    if T = U then ((v, (u, maxidx_u)), (thy', sorts'))
+    else
+      raise TYPE (Pretty.string_of (Pretty.block
        [Pretty.str "instantiate: type conflict",
-        Pretty.fbrk, pretty_typing thy' t T,
-        Pretty.fbrk, pretty_typing thy' u U]), [T, U], [t, u])
-    | _ => raise TYPE (Pretty.string_of (Pretty.block
-       [Pretty.str "instantiate: not a variable",
-        Pretty.fbrk, Syntax.pretty_term_global thy' t]), [], [t]))
+        Pretty.fbrk, pretty_typing thy' (Var v) T,
+        Pretty.fbrk, pretty_typing thy' u U]), [T, U], [Var v, u])
   end;
 
-fun add_instT (cT, cU) (thy, sorts) =
+fun add_instT (v as (_, S), cU) (thy, sorts) =
   let
-    val Ctyp {T, thy = thy1, ...} = cT
-    and Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
-    val thy' = Theory.merge (thy, Theory.merge (thy1, thy2));
+    val Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
+    val thy' = Theory.merge (thy, thy2);
     val sorts' = Sorts.union sorts_U sorts;
   in
-    (case T of TVar (v as (_, S)) =>
-      if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts'))
-      else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
-    | _ => raise TYPE (Pretty.string_of (Pretty.block
-        [Pretty.str "instantiate: not a type variable",
-         Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], []))
+    if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts'))
+    else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
   end;
 
 in