src/HOL/cladata.ML
changeset 9846 bb848beb53f6
parent 9531 7a0d4a6299b4
child 9969 4753185f1dd2
     1.1 --- a/src/HOL/cladata.ML	Tue Sep 05 18:43:05 2000 +0200
     1.2 +++ b/src/HOL/cladata.ML	Tue Sep 05 18:43:22 2000 +0200
     1.3 @@ -32,12 +32,7 @@
     1.4  
     1.5  
     1.6  (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
     1.7 -structure Make_Elim_Data =
     1.8 -struct
     1.9 -  val classical = classical
    1.10 -end;
    1.11 -
    1.12 -structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
    1.13 +structure Make_Elim = Make_Elim_Fun (val classical = classical);
    1.14  
    1.15  (*we don't redeclare the original make_elim (Tactic.make_elim) for 
    1.16    compatibliity with strange things done in many existing proofs *)