src/Tools/induct.ML
changeset 32032 a6a6e8031c14
parent 30722 623d4831c8cf
child 32091 30e2ffbba718
     1.1 --- a/src/Tools/induct.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/Tools/induct.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -423,14 +423,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun dest_env thy (env as Envir.Envir {iTs, ...}) =
     1.8 +fun dest_env thy env =
     1.9    let
    1.10      val cert = Thm.cterm_of thy;
    1.11      val certT = Thm.ctyp_of thy;
    1.12 -    val pairs = Envir.alist_of env;
    1.13 +    val pairs = Vartab.dest (Envir.term_env env);
    1.14 +    val types = Vartab.dest (Envir.type_env env);
    1.15      val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
    1.16      val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
    1.17 -  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
    1.18 +  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
    1.19  
    1.20  in
    1.21  
    1.22 @@ -450,8 +451,7 @@
    1.23          val rule' = Thm.incr_indexes (maxidx + 1) rule;
    1.24          val concl = Logic.strip_assums_concl goal;
    1.25        in
    1.26 -        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
    1.27 -          (Envir.empty (#maxidx (Thm.rep_thm rule')))
    1.28 +        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
    1.29          |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
    1.30        end
    1.31    end handle Subscript => Seq.empty;