src/HOL/Tools/typedef_package.ML
changeset 9969 4753185f1dd2
parent 9315 f793f05024f6
child 10280 2626d4e37341
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Sep 15 11:34:46 2000 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Sep 15 12:39:57 2000 +0200
     1.3 @@ -193,7 +193,7 @@
     1.4  (* typedef_proof interface *)
     1.5  
     1.6  fun typedef_attribute cset do_typedef (thy, thm) =
     1.7 -  (check_nonempty cset (thm RS (select_eq_Ex RS iffD2)); (thy |> do_typedef, thm));
     1.8 +  (check_nonempty cset (thm RS (some_eq_ex RS iffD2)); (thy |> do_typedef, thm));
     1.9  
    1.10  fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
    1.11    let