src/Pure/Isar/proof.ML
changeset 6887 12b5fb35a688
parent 6876 4ae9c47f2b6b
child 6891 7bb02d03035d
equal deleted inserted replaced
6886:7d0f7ad5a35f 6887:12b5fb35a688
   327     fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None
   327     fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None
   328       | get_free _ (opt, _) = opt;
   328       | get_free _ (opt, _) = opt;
   329 
   329 
   330     fun find_free t x = foldl_aterms (get_free x) (None, t);
   330     fun find_free t x = foldl_aterms (get_free x) (None, t);
   331 
   331 
   332     val {sign, maxidx, prop, ...} = Thm.rep_thm thm;
   332     val {sign, prop, ...} = Thm.rep_thm thm;
   333     val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names);
   333     val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names);
   334   in
   334   in
   335     thm
   335     thm
   336     |> Drule.forall_intr_list frees
   336     |> Drule.forall_intr_list frees
   337     |> Drule.forall_elim_vars (maxidx + 1)
   337     |> Drule.forall_elim_vars 0
   338   end;
   338   end;
   339 
   339 
   340 fun varify_tfrees thm =
   340 fun varify_tfrees thm =
   341   let
   341   let
   342     val {hyps, prop, ...} = Thm.rep_thm thm;
   342     val {hyps, prop, ...} = Thm.rep_thm thm;