src/ZF/arith_data.ML
changeset 32155 e2bf2f73b0c8
parent 29269 5c25a2012975
child 33317 b4534348b8fd
     1.1 --- a/src/ZF/arith_data.ML	Thu Jul 23 22:20:37 2009 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Thu Jul 23 23:12:21 2009 +0200
     1.3 @@ -76,8 +76,8 @@
     1.4          (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
     1.5    end;
     1.6  
     1.7 -fun prep_simproc (name, pats, proc) =
     1.8 -  Simplifier.simproc (the_context ()) name pats proc;
     1.9 +fun prep_simproc thy (name, pats, proc) =
    1.10 +  Simplifier.simproc thy name pats proc;
    1.11  
    1.12  
    1.13  (*** Use CancelNumerals simproc without binary numerals,
    1.14 @@ -198,7 +198,7 @@
    1.15  
    1.16  
    1.17  val nat_cancel =
    1.18 -  map prep_simproc
    1.19 +  map (prep_simproc @{theory})
    1.20     [("nateq_cancel_numerals",
    1.21       ["l #+ m = n", "l = m #+ n",
    1.22        "l #* m = n", "l = m #* n",