src/Pure/simplifier.ML
changeset 16685 4ffc943c9c75
parent 16684 7b58002668c0
child 16709 a4679ac06502
     1.1 --- a/src/Pure/simplifier.ML	Mon Jul 04 20:13:39 2005 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Mon Jul 04 20:20:50 2005 +0200
     1.3 @@ -475,10 +475,10 @@
     1.4    Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
     1.5    Scan.succeed asm_full_simp_tac);
     1.6  
     1.7 -val simp_flags = Scan.repeat
     1.8 +fun simp_flags x = (Scan.repeat
     1.9    (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat)
    1.10      >> setmp MetaSimplifier.simp_depth_limit)
    1.11 -  >> curry (Library.foldl op o) I;
    1.12 +  >> curry (Library.foldl op o) I) x;
    1.13  
    1.14  val cong_modifiers =
    1.15   [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),