src/Tools/IsaPlanner/isand.ML
changeset 26653 60e0cf6bef89
parent 23175 267ba70e7a9d
child 29265 5b4247055bd7
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Tue Apr 15 16:12:01 2008 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Tue Apr 15 16:12:05 2008 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4        val ct = ctermify allified_term;
     1.5        val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
     1.6      in (typ_allified_ct, 
     1.7 -        Drule.forall_elim_vars 0 (Thm.assume ct)) end;
     1.8 +        Thm.forall_elim_vars 0 (Thm.assume ct)) end;
     1.9  
    1.10  
    1.11  (* change type-vars to fresh type frees *)
    1.12 @@ -271,7 +271,7 @@
    1.13  
    1.14  (* make free vars into schematic vars with index zero *)
    1.15   fun unfix_frees frees = 
    1.16 -     apply (map (K (Drule.forall_elim_var 0)) frees) 
    1.17 +     apply (map (K (Thm.forall_elim_var 0)) frees) 
    1.18       o Drule.forall_intr_list frees;
    1.19  
    1.20  (* fix term and type variables *)