src/Tools/IsaPlanner/isand.ML
changeset 46777 1ce61ee1571a
parent 46217 7b19666f0e3d
child 49339 d1fcb4de8349
equal deleted inserted replaced
46776:8575cc482dfb 46777:1ce61ee1571a
   268     in Thm.instantiate ([], cfixes) th end;
   268     in Thm.instantiate ([], cfixes) th end;
   269 
   269 
   270 
   270 
   271 (* make free vars into schematic vars with index zero *)
   271 (* make free vars into schematic vars with index zero *)
   272  fun unfix_frees frees = 
   272  fun unfix_frees frees = 
   273      apply (map (K (Thm.forall_elim_var 0)) frees) 
   273      fold (K (Thm.forall_elim_var 0)) frees
   274      o Drule.forall_intr_list frees;
   274      o Drule.forall_intr_list frees;
   275 
   275 
   276 (* fix term and type variables *)
   276 (* fix term and type variables *)
   277 fun fix_vars_and_tvars th = 
   277 fun fix_vars_and_tvars th = 
   278     let val (tvars, th') = fix_tvars_to_tfrees th
   278     let val (tvars, th') = fix_tvars_to_tfrees th