src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
changeset 66020 a31760eee09d
parent 61756 21c2b1f691d1
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Jun 05 23:55:58 2017 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Jun 06 13:13:25 2017 +0200
     1.3 @@ -300,7 +300,7 @@
     1.4        (s ^ (term
     1.5              |> singleton (Syntax.uncheck_terms ctxt)
     1.6              |> annotate_types_in_term ctxt
     1.7 -            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
     1.8 +            |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
     1.9              |> simplify_spaces
    1.10              |> maybe_quote keywords),
    1.11         ctxt |> perhaps (try (Variable.auto_fixes term)))
    1.12 @@ -320,7 +320,7 @@
    1.13  
    1.14      fun of_free (s, T) =
    1.15        maybe_quote keywords s ^ " :: " ^
    1.16 -      maybe_quote keywords (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
    1.17 +      maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
    1.18  
    1.19      fun add_frees xs (s, ctxt) =
    1.20        (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))