eq_prop: Envir.beta_eta_contract;
authorwenzelm
Mon Feb 06 20:59:47 2006 +0100 (2006-02-06)
changeset 18947de38ee3654d4
parent 18946 ce65d2d2e0c2
child 18948 b6b19cc8454f
eq_prop: Envir.beta_eta_contract;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Mon Feb 06 20:59:46 2006 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Mon Feb 06 20:59:47 2006 +0100
     1.3 @@ -128,7 +128,7 @@
     1.4  fun calculate prep_rules final raw_rules int state =
     1.5    let
     1.6      val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
     1.7 -    val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
     1.8 +    val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
     1.9      fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
    1.10  
    1.11      val opt_rules = Option.map (prep_rules state) raw_rules;