# HG changeset patch
# User wenzelm
# Date 1175638276 -7200
# Node ID d0f0f37ec34633f556345651bec3a3e20afae51b
# Parent  4b1ecb19b411e542d65af9ce71e9091b218c5dd3
improved exception CTERM;
added instantiate_cterm;
removed obsolete sign_of_thm;

diff -r 4b1ecb19b411 -r d0f0f37ec346 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 04 00:11:14 2007 +0200
+++ b/src/Pure/thm.ML	Wed Apr 04 00:11:16 2007 +0200
@@ -24,7 +24,7 @@
 
   (*certified terms*)
   type cterm
-  exception CTERM of string
+  exception CTERM of string * cterm list
   val rep_cterm: cterm ->
    {thy: theory,
     sign: theory,       (*obsolete*)
@@ -74,7 +74,6 @@
     prop: cterm}
   exception THM of string * int * thm list
   val theory_of_thm: thm -> theory
-  val sign_of_thm: thm -> theory    (*obsolete*)
   val prop_of: thm -> term
   val proof_of: thm -> Proofterm.proof
   val tpairs_of: thm -> (term * term) list
@@ -112,6 +111,7 @@
   val flexflex_rule: 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 trivial: cterm -> thm
   val class_triv: theory -> class -> thm
   val unconstrainT: ctyp -> thm -> thm
@@ -229,7 +229,7 @@
   sorts: sort list}
 with
 
-exception CTERM of string;
+exception CTERM of string * cterm list;
 
 fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
   let val thy =  Theory.deref thy_ref
@@ -258,34 +258,35 @@
   Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise TERM (msg, [t1, t2]);
 
 
-fun dest_comb (Cterm {t = t $ u, T, thy_ref, maxidx, sorts}) =
+fun dest_comb (ct as Cterm {t = t $ u, T, thy_ref, maxidx, sorts}) =
       let val A = Term.argument_type_of t in
         (Cterm {t = t, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
          Cterm {t = u, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
       end
-  | dest_comb _ = raise CTERM "dest_comb";
+  | dest_comb ct = raise CTERM ("dest_comb", [ct]);
 
-fun dest_arg (Cterm {t = t $ u, T, thy_ref, maxidx, sorts}) =
+fun dest_arg (ct as Cterm {t = t $ u, T, thy_ref, maxidx, sorts}) =
       let val A = Term.argument_type_of t in
          Cterm {t = u, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}
       end
-  | dest_arg _ = raise CTERM "dest_arg";
+  | dest_arg ct = raise CTERM ("dest_arg", [ct]);
 
-fun dest_binop (Cterm {t = tm, T = _, thy_ref, maxidx, sorts}) =
+fun dest_binop (ct as Cterm {t = tm, T = _, thy_ref, maxidx, sorts}) =
   let fun cterm t T = Cterm {t = t, T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} in
     (case tm of
       Const (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
     |  Free (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
     |   Var (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
-    | _ => raise CTERM "dest_binop")
+    | _ => raise CTERM ("dest_binop", [ct]))
   end;
 
-fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
+fun dest_abs a (ct as
+        Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
       let val (y', t') = Term.dest_abs (the_default x a, T, t) in
         (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
           Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
       end
-  | dest_abs _ _ = raise CTERM "dest_abs";
+  | dest_abs _ ct = raise CTERM ("dest_abs", [ct]);
 
 fun capply
   (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
@@ -296,8 +297,8 @@
         T = rty,
         maxidx = Int.max (maxidx1, maxidx2),
         sorts = Sorts.union sorts1 sorts2}
-      else raise CTERM "capply: types don't agree"
-  | capply _ _ = raise CTERM "capply: first arg is not a function"
+      else raise CTERM ("capply: types don't agree", [cf, cx])
+  | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);
 
 fun cabs
   (ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
@@ -340,7 +341,7 @@
 
 (*Incrementing indexes*)
 fun cterm_incr_indexes i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
-  if i < 0 then raise CTERM "negative increment"
+  if i < 0 then raise CTERM ("negative increment", [ct])
   else if i = 0 then ct
   else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t,
     T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
@@ -432,8 +433,6 @@
 (* basic components *)
 
 fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref;
-val sign_of_thm = theory_of_thm;
-
 fun maxidx_of (Thm {maxidx, ...}) = maxidx;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
 fun hyps_of (Thm {hyps, ...}) = hyps;
@@ -1024,7 +1023,7 @@
       end;
 
 
-(*Instantiation of Vars
+(*Instantiation of schematic variables
            A
   --------------------
   A[t1/v1, ..., tn/vn]
@@ -1097,6 +1096,19 @@
       end
       handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
 
+fun instantiate_cterm ([], []) ct = ct
+  | instantiate_cterm (instT, inst) ct =
+      let
+        val Cterm {thy_ref, t, T, sorts, ...} = ct;
+        val (inst', (instT', (thy_ref', sorts'))) =
+          (thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
+        val subst = TermSubst.instantiate_maxidx (instT', inst');
+        val substT = TermSubst.instantiateT_maxidx instT';
+        val (t', maxidx1) = subst t ~1;
+        val (T', maxidx') = substT T maxidx1;
+      in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
+      handle TYPE (msg, _, _) => raise CTERM (msg, [ct]);
+
 end;