src/Pure/Isar/proof_context.ML
changeset 26722 a239220108a5
parent 26717 2e1c3a0e7308
child 26731 48df747c8543
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 18 23:49:44 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 18 23:49:46 2008 +0200
     1.3 @@ -1189,7 +1189,9 @@
     1.4  
     1.5  (* local contexts *)
     1.6  
     1.7 -fun pretty_cases ctxt =
     1.8 +local
     1.9 +
    1.10 +fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) =
    1.11    let
    1.12      val prt_term = Syntax.pretty_term ctxt;
    1.13  
    1.14 @@ -1203,27 +1205,34 @@
    1.15      fun prt_sect _ _ _ [] = []
    1.16        | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s ::
    1.17              flat (Library.separate sep (map (Library.single o prt) xs))))];
    1.18 -
    1.19 -    fun prt_case (name, (fixes, (asms, (lets, cs)))) = Pretty.block (Pretty.fbreaks
    1.20 +  in
    1.21 +    Pretty.block (Pretty.fbreaks
    1.22        (Pretty.str (name ^ ":") ::
    1.23          prt_sect "fix" [] (Pretty.str o fst) fixes @
    1.24          prt_sect "let" [Pretty.str "and"] prt_let
    1.25            (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
    1.26          (if forall (null o #2) asms then []
    1.27            else prt_sect "assume" [Pretty.str "and"] prt_asm asms) @
    1.28 -        prt_sect "subcases:" [] (Pretty.str o fst) cs));
    1.29 +        prt_sect "subcases:" [] (Pretty.str o fst) cs))
    1.30 +  end;
    1.31  
    1.32 +in
    1.33 +
    1.34 +fun pretty_cases ctxt =
    1.35 +  let
    1.36      fun add_case (_, (_, false)) = I
    1.37        | add_case (name, (c as RuleCases.Case {fixes, ...}, true)) =
    1.38 -          cons (name, (fixes, #1 (case_result c ctxt)));
    1.39 +          cons (name, (fixes, case_result c ctxt));
    1.40      val cases = fold add_case (cases_of ctxt) [];
    1.41    in
    1.42      if null cases andalso not (! verbose) then []
    1.43 -    else [Pretty.big_list "cases:" (map prt_case cases)]
    1.44 +    else [Pretty.big_list "cases:" (map pretty_case cases)]
    1.45    end;
    1.46  
    1.47  val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
    1.48  
    1.49 +end;
    1.50 +
    1.51  
    1.52  (* core context *)
    1.53