src/Pure/Isar/proof_context.ML
changeset 26939 1035c89b4c02
parent 26930 64e50d783276
child 26960 1aa5cd390dfb
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -284,7 +284,7 @@
     1.4  
     1.5  fun pretty_thm_legacy th =
     1.6    let val thy = Thm.theory_of_thm th
     1.7 -  in Display.pretty_thm_aux (Syntax.pp (init thy)) true false [] th end;
     1.8 +  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
     1.9  
    1.10  fun pretty_thm ctxt th =
    1.11    let val asms = map Thm.term_of (Assumption.assms_of ctxt)
    1.12 @@ -365,7 +365,7 @@
    1.13    (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
    1.14     else Pretty.mark Markup.free (Pretty.str x))
    1.15    |> Pretty.mark
    1.16 -    (if Variable.is_fixed ctxt x orelse Sign.is_pretty_global ctxt then Markup.fixed x
    1.17 +    (if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x
    1.18       else Markup.hilite);
    1.19  
    1.20  fun var_or_skolem _ s =