src/ZF/arith_data.ML
changeset 38715 6513ea67d95d
parent 38513 33ab01218ae1
child 40878 7695e4de4d86
equal deleted inserted replaced
38714:31da698fc4e5 38715:6513ea67d95d
    75       handle ERROR msg =>
    75       handle ERROR msg =>
    76         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
    76         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
    77   end;
    77   end;
    78 
    78 
    79 fun prep_simproc thy (name, pats, proc) =
    79 fun prep_simproc thy (name, pats, proc) =
    80   Simplifier.simproc thy name pats proc;
    80   Simplifier.simproc_global thy name pats proc;
    81 
    81 
    82 
    82 
    83 (*** Use CancelNumerals simproc without binary numerals,
    83 (*** Use CancelNumerals simproc without binary numerals,
    84      just for cancellation ***)
    84      just for cancellation ***)
    85 
    85