1.1 --- a/src/HOL/Tools/meson.ML	Tue Apr 17 21:06:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Apr 18 11:14:09 2007 +0200
     1.3 @@ -541,11 +541,6 @@
     1.4      cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
     1.5      REPEAT o (etac exE);
     1.6  
     1.7 -(*Expand all definitions (presumably of Skolem functions) in a proof state.*)
     1.8 -fun expand_defs_tac st =
     1.9 -  let val defs = filter (can dest_equals) (#hyps (crep_thm st))
    1.10 -  in  PRIMITIVE (LocalDefs.expand defs) st  end;
    1.11 -
    1.12  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
    1.13    Function mkcl converts theorems to clauses.*)
    1.14  fun MESON mkcl cltac i st = 
    1.15 @@ -553,9 +548,8 @@
    1.16      (EVERY [rtac ccontr 1,
    1.17  	    METAHYPS (fn negs =>
    1.18  		      EVERY1 [skolemize_prems_tac negs,
    1.19 -			      METAHYPS (cltac o mkcl)]) 1,
    1.20 -            expand_defs_tac]) i st
    1.21 -  handle THM _ => no_tac st;	(*probably from make_meta_clause, not first-order*)		      
    1.22 +			      METAHYPS (cltac o mkcl)]) 1]) i st
    1.23 +  handle THM _ => no_tac st;	(*probably from make_meta_clause, not first-order*)
    1.24  
    1.25  (** Best-first search versions **)
    1.26