src/HOL/Nominal/nominal_fresh_fun.ML
changeset 47060 e2741ec9ae36
parent 46219 426ed18eba43
child 51669 7fbc4fc400d8
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Mar 20 21:37:31 2012 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 21 11:00:34 2012 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
     1.5     rtac fs_name_thm 1 THEN
     1.6     etac exE 1) thm
     1.7 -  handle Empty  => all_tac thm (* if we collected no variables then we do nothing *)
     1.8 +  handle List.Empty  => all_tac thm (* if we collected no variables then we do nothing *)
     1.9    end;
    1.10  
    1.11  fun get_inner_fresh_fun (Bound j) = NONE