src/Pure/drule.ML
changeset 6930 4b40fb299f9f
parent 6435 154b88d2b62e
child 6946 309276732ee1
     1.1 --- a/src/Pure/drule.ML	Thu Jul 08 18:30:21 1999 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Jul 08 18:31:04 1999 +0200
     1.3 @@ -386,7 +386,7 @@
     1.4    in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
     1.5    handle TERM _ =>
     1.6             raise THM("cterm_instantiate: incompatible signatures",0,[th])
     1.7 -       | TYPE (msg, _, _) => raise THM("cterm_instantiate: " ^ msg, 0, [th])
     1.8 +       | TYPE (msg, _, _) => raise THM(msg, 0, [th])
     1.9  end;
    1.10  
    1.11  
    1.12 @@ -680,7 +680,9 @@
    1.13  
    1.14          fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S)));
    1.15          fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T)));
    1.16 -      in instantiate' (map inc_tvar (tvars_of thm)) (map inc_var (vars_of thm)) thm end;
    1.17 +        val thm' = instantiate' (map inc_tvar (tvars_of thm)) [] thm;
    1.18 +        val thm'' = instantiate' [] (map inc_var (vars_of thm')) thm';
    1.19 +      in thm'' end;
    1.20  
    1.21  fun incr_indexes_wrt is cTs cts thms =
    1.22    let