Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
improved error msgs of cterm_instantiate;
authorwenzelm
Thu, 08 Jul 1999 18:31:04 +0200
changeset 6930 4b40fb299f9f
parent 6929 16ee7b14a2c1
child 6931 bd8aa6ae6bcd
improved error msgs of cterm_instantiate; fixed incr_indexes;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/drule.ML	Thu Jul 08 18:30:21 1999 +0200
+++ b/src/Pure/drule.ML	Thu Jul 08 18:31:04 1999 +0200
@@ -386,7 +386,7 @@
   in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   handle TERM _ =>
            raise THM("cterm_instantiate: incompatible signatures",0,[th])
-       | TYPE (msg, _, _) => raise THM("cterm_instantiate: " ^ msg, 0, [th])
+       | TYPE (msg, _, _) => raise THM(msg, 0, [th])
 end;
 
 
@@ -680,7 +680,9 @@
 
         fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S)));
         fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T)));
-      in instantiate' (map inc_tvar (tvars_of thm)) (map inc_var (vars_of thm)) thm end;
+        val thm' = instantiate' (map inc_tvar (tvars_of thm)) [] thm;
+        val thm'' = instantiate' [] (map inc_var (vars_of thm')) thm';
+      in thm'' end;
 
 fun incr_indexes_wrt is cTs cts thms =
   let
isabelle