src/Pure/Tools/find_consts.ML
changeset 60667 d86c449d30ba
parent 60664 263a8f15faf3
child 61223 dfccf6c06201
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Jul 06 16:03:01 2015 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Jul 06 16:10:00 2015 +0200
     1.3 @@ -49,10 +49,11 @@
     1.4  fun pretty_criterion (b, c) =
     1.5    let
     1.6      fun prfx s = if b then s else "-" ^ s;
     1.7 +    val show_pat = quote o Input.source_content o Syntax.read_input;
     1.8    in
     1.9      (case c of
    1.10 -      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    1.11 -    | Loose pat => Pretty.str (prfx (quote pat))
    1.12 +      Strict pat => Pretty.str (prfx "strict: " ^ show_pat pat)
    1.13 +    | Loose pat => Pretty.str (prfx (show_pat pat))
    1.14      | Name name => Pretty.str (prfx "name: " ^ quote name))
    1.15    end;
    1.16