src/HOL/cladata.ML
changeset 11753 02b257ef0ee2
parent 11451 8abfb4f7bd02
child 12355 c8d3c3d09080
     1.1 --- a/src/HOL/cladata.ML	Sun Oct 14 20:02:30 2001 +0200
     1.2 +++ b/src/HOL/cladata.ML	Sun Oct 14 20:02:59 2001 +0200
     1.3 @@ -38,10 +38,6 @@
     1.4    compatibliity with strange things done in many existing proofs *)
     1.5  val cla_make_elim = Make_Elim.make_elim;
     1.6  
     1.7 -val atomize_rules = thms "atomize'";
     1.8 -val atomize_tac = Method.atomize_tac atomize_rules;
     1.9 -val atomize_strip_tac = Method.atomize_strip_tac (atomize_rules, [impI, allI]);
    1.10 -
    1.11  (*** Applying ClassicalFun to create a classical prover ***)
    1.12  structure Classical_Data = 
    1.13    struct
    1.14 @@ -51,7 +47,6 @@
    1.15    val classical = classical
    1.16    val sizef     = size_of_thm
    1.17    val hyp_subst_tacs=[hyp_subst_tac]
    1.18 -  val atomize	= atomize_rules
    1.19    end;
    1.20  
    1.21  structure Classical = ClassicalFun(Classical_Data);