merged
authorwenzelm
Wed Aug 11 18:17:53 2010 +0200 (2010-08-11 ago)
changeset 38351ea1ee55aa41f
parent 38350 480b2de9927c
parent 38337 f6c1e169f51b
child 38352 4c8bcb826e83
merged
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Aug 11 14:45:38 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Aug 11 18:17:53 2010 +0200
     1.3 @@ -830,10 +830,10 @@
     1.4            str "case Seq.pull (testf p) of", Pretty.brk 1,
     1.5            str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
     1.6            str " =>", Pretty.brk 1, str "SOME ",
     1.7 -          Pretty.block (str "[" ::
     1.8 -            Pretty.commas (map (fn (s, T) => Pretty.block
     1.9 -              [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
    1.10 -            [str "]"]), Pretty.brk 1,
    1.11 +          Pretty.enum "," "[" "]"
    1.12 +            (map (fn (s, T) => Pretty.block
    1.13 +              [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'),
    1.14 +          Pretty.brk 1,
    1.15            str "| NONE => NONE);"]) ^
    1.16        "\n\nend;\n";
    1.17      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
     2.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 11 14:45:38 2010 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 11 18:17:53 2010 +0200
     2.3 @@ -16,7 +16,6 @@
     2.4    val defined: theory -> string -> bool
     2.5    val attribute: theory -> src -> attribute
     2.6    val attribute_i: theory -> src -> attribute
     2.7 -  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
     2.8    val map_specs: ('a -> 'att) ->
     2.9      (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
    2.10    val map_facts: ('a -> 'att) ->
    2.11 @@ -25,6 +24,7 @@
    2.12    val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
    2.13      (('c * 'a list) * ('b * 'a list) list) list ->
    2.14      (('c * 'att list) * ('fact * 'att list) list) list
    2.15 +  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    2.16    val crude_closure: Proof.context -> src -> src
    2.17    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    2.18    val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    2.19 @@ -94,8 +94,7 @@
    2.20  
    2.21  fun pretty_attribs _ [] = []
    2.22    | pretty_attribs ctxt srcs =
    2.23 -      [Pretty.enclose "[" "]"
    2.24 -        (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
    2.25 +      [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
    2.26  
    2.27  
    2.28  (* get attributes *)
    2.29 @@ -115,11 +114,6 @@
    2.30  
    2.31  fun attribute thy = attribute_i thy o intern_src thy;
    2.32  
    2.33 -fun eval_thms ctxt args = ProofContext.note_thmss ""
    2.34 -    [(Thm.empty_binding, args |> map (fn (a, atts) =>
    2.35 -        (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
    2.36 -  |> fst |> maps snd;
    2.37 -
    2.38  
    2.39  (* attributed declarations *)
    2.40  
    2.41 @@ -129,6 +123,15 @@
    2.42  fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
    2.43  
    2.44  
    2.45 +(* fact expressions *)
    2.46 +
    2.47 +fun eval_thms ctxt srcs = ctxt
    2.48 +  |> ProofContext.note_thmss ""
    2.49 +    (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
    2.50 +      [((Binding.empty, []), srcs)])
    2.51 +  |> fst |> maps snd;
    2.52 +
    2.53 +
    2.54  (* crude_closure *)
    2.55  
    2.56  (*Produce closure without knowing facts in advance! The following
     3.1 --- a/src/Pure/Isar/calculation.ML	Wed Aug 11 14:45:38 2010 +0200
     3.2 +++ b/src/Pure/Isar/calculation.ML	Wed Aug 11 18:17:53 2010 +0200
     3.3 @@ -37,8 +37,10 @@
     3.4      ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
     3.5  );
     3.6  
     3.7 +val get_rules = #1 o Data.get o Context.Proof;
     3.8 +
     3.9  fun print_rules ctxt =
    3.10 -  let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
    3.11 +  let val (trans, sym) = get_rules ctxt in
    3.12      [Pretty.big_list "transitivity rules:"
    3.13          (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
    3.14        Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
    3.15 @@ -122,21 +124,21 @@
    3.16  
    3.17  (* also and finally *)
    3.18  
    3.19 -val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
    3.20 -
    3.21  fun calculate prep_rules final raw_rules int state =
    3.22    let
    3.23 +    val ctxt = Proof.context_of state;
    3.24 +
    3.25      val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
    3.26      val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
    3.27      fun projection ths th = exists (curry eq_prop th) ths;
    3.28  
    3.29 -    val opt_rules = Option.map (prep_rules state) raw_rules;
    3.30 +    val opt_rules = Option.map (prep_rules ctxt) raw_rules;
    3.31      fun combine ths =
    3.32        (case opt_rules of SOME rules => rules
    3.33        | NONE =>
    3.34            (case ths of
    3.35 -            [] => Item_Net.content (#1 (get_rules state))
    3.36 -          | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
    3.37 +            [] => Item_Net.content (#1 (get_rules ctxt))
    3.38 +          | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
    3.39        |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
    3.40        |> Seq.filter (not o projection ths);
    3.41  
    3.42 @@ -154,9 +156,9 @@
    3.43    end;
    3.44  
    3.45  val also = calculate (K I) false;
    3.46 -val also_cmd = calculate Proof.get_thmss_cmd false;
    3.47 +val also_cmd = calculate Attrib.eval_thms false;
    3.48  val finally = calculate (K I) true;
    3.49 -val finally_cmd = calculate Proof.get_thmss_cmd true;
    3.50 +val finally_cmd = calculate Attrib.eval_thms true;
    3.51  
    3.52  
    3.53  (* moreover and ultimately *)
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 11 14:45:38 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Aug 11 18:17:53 2010 +0200
     4.3 @@ -416,7 +416,7 @@
     4.4  
     4.5  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
     4.6    Thm_Deps.thm_deps (Toplevel.theory_of state)
     4.7 -    (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
     4.8 +    (Attrib.eval_thms (Toplevel.context_of state) args));
     4.9  
    4.10  
    4.11  (* find unused theorems *)
    4.12 @@ -450,20 +450,20 @@
    4.13  
    4.14  local
    4.15  
    4.16 -fun string_of_stmts state args =
    4.17 -  Proof.get_thmss_cmd state args
    4.18 -  |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
    4.19 +fun string_of_stmts ctxt args =
    4.20 +  Attrib.eval_thms ctxt args
    4.21 +  |> map (Element.pretty_statement ctxt Thm.theoremK)
    4.22    |> Pretty.chunks2 |> Pretty.string_of;
    4.23  
    4.24 -fun string_of_thms state args =
    4.25 -  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
    4.26 +fun string_of_thms ctxt args =
    4.27 +  Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
    4.28  
    4.29  fun string_of_prfs full state arg =
    4.30    Pretty.string_of
    4.31      (case arg of
    4.32        NONE =>
    4.33          let
    4.34 -          val {context = ctxt, goal = thm} = Proof.simple_goal state;
    4.35 +          val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
    4.36            val thy = ProofContext.theory_of ctxt;
    4.37            val prf = Thm.proof_of thm;
    4.38            val prop = Thm.full_prop_of thm;
    4.39 @@ -472,20 +472,19 @@
    4.40            Proof_Syntax.pretty_proof ctxt
    4.41              (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
    4.42          end
    4.43 -    | SOME args => Pretty.chunks
    4.44 -        (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
    4.45 -          (Proof.get_thmss_cmd state args)));
    4.46 +    | SOME srcs =>
    4.47 +        let val ctxt = Toplevel.context_of state
    4.48 +        in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
    4.49 +        |> Pretty.chunks);
    4.50  
    4.51 -fun string_of_prop state s =
    4.52 +fun string_of_prop ctxt s =
    4.53    let
    4.54 -    val ctxt = Proof.context_of state;
    4.55      val prop = Syntax.read_prop ctxt s;
    4.56      val ctxt' = Variable.auto_fixes prop ctxt;
    4.57    in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
    4.58  
    4.59 -fun string_of_term state s =
    4.60 +fun string_of_term ctxt s =
    4.61    let
    4.62 -    val ctxt = Proof.context_of state;
    4.63      val t = Syntax.read_term ctxt s;
    4.64      val T = Term.type_of t;
    4.65      val ctxt' = Variable.auto_fixes t ctxt;
    4.66 @@ -495,24 +494,21 @@
    4.67          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
    4.68    end;
    4.69  
    4.70 -fun string_of_type state s =
    4.71 -  let
    4.72 -    val ctxt = Proof.context_of state;
    4.73 -    val T = Syntax.read_typ ctxt s;
    4.74 +fun string_of_type ctxt s =
    4.75 +  let val T = Syntax.read_typ ctxt s
    4.76    in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
    4.77  
    4.78  fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
    4.79 -  Print_Mode.with_modes modes (fn () =>
    4.80 -    writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
    4.81 +  Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
    4.82  
    4.83  in
    4.84  
    4.85 -val print_stmts = print_item string_of_stmts;
    4.86 -val print_thms = print_item string_of_thms;
    4.87 +val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
    4.88 +val print_thms = print_item (string_of_thms o Toplevel.context_of);
    4.89  val print_prfs = print_item o string_of_prfs;
    4.90 -val print_prop = print_item string_of_prop;
    4.91 -val print_term = print_item string_of_term;
    4.92 -val print_type = print_item string_of_type;
    4.93 +val print_prop = print_item (string_of_prop o Toplevel.context_of);
    4.94 +val print_term = print_item (string_of_term o Toplevel.context_of);
    4.95 +val print_type = print_item (string_of_type o Toplevel.context_of);
    4.96  
    4.97  end;
    4.98  
     5.1 --- a/src/Pure/Isar/proof.ML	Wed Aug 11 14:45:38 2010 +0200
     5.2 +++ b/src/Pure/Isar/proof.ML	Wed Aug 11 18:17:53 2010 +0200
     5.3 @@ -60,7 +60,6 @@
     5.4    val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
     5.5    val chain: state -> state
     5.6    val chain_facts: thm list -> state -> state
     5.7 -  val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
     5.8    val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
     5.9    val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
    5.10    val from_thmss: ((thm list * attribute list) list) list -> state -> state
    5.11 @@ -679,8 +678,6 @@
    5.12  
    5.13  val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
    5.14  
    5.15 -fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
    5.16 -
    5.17  end;
    5.18  
    5.19  
     6.1 --- a/src/Pure/Isar/proof_context.ML	Wed Aug 11 14:45:38 2010 +0200
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Aug 11 18:17:53 2010 +0200
     6.3 @@ -1123,7 +1123,7 @@
     6.4  val type_notation = gen_notation (K type_syntax);
     6.5  val notation = gen_notation const_syntax;
     6.6  
     6.7 -fun target_type_notation add  mode args phi =
     6.8 +fun target_type_notation add mode args phi =
     6.9    let
    6.10      val args' = args |> map_filter (fn (T, mx) =>
    6.11        let
     7.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 14:45:38 2010 +0200
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:17:53 2010 +0200
     7.3 @@ -20,7 +20,6 @@
     7.4    val theory_of: state -> theory
     7.5    val proof_of: state -> Proof.state
     7.6    val proof_position_of: state -> int
     7.7 -  val enter_proof_body: state -> Proof.state
     7.8    val end_theory: Position.T -> state -> theory
     7.9    val print_state_context: state -> unit
    7.10    val print_state: bool -> state -> unit
    7.11 @@ -186,8 +185,6 @@
    7.12      Proof (prf, _) => Proof_Node.position prf
    7.13    | _ => raise UNDEF);
    7.14  
    7.15 -val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
    7.16 -
    7.17  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
    7.18    | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
    7.19  
     8.1 --- a/src/Pure/Syntax/ast.ML	Wed Aug 11 14:45:38 2010 +0200
     8.2 +++ b/src/Pure/Syntax/ast.ML	Wed Aug 11 18:17:53 2010 +0200
     8.3 @@ -75,8 +75,7 @@
     8.4  
     8.5  fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
     8.6    | pretty_ast (Variable x) = Pretty.str x
     8.7 -  | pretty_ast (Appl asts) =
     8.8 -      Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
     8.9 +  | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
    8.10  
    8.11  fun pretty_rule (lhs, rhs) =
    8.12    Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
     9.1 --- a/src/Pure/Tools/find_consts.ML	Wed Aug 11 14:45:38 2010 +0200
     9.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Aug 11 18:17:53 2010 +0200
     9.3 @@ -28,24 +28,13 @@
     9.4  (* matching types/consts *)
     9.5  
     9.6  fun matches_subtype thy typat =
     9.7 -  let
     9.8 -    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
     9.9 -
    9.10 -    fun fs [] = false
    9.11 -      | fs (t :: ts) = f t orelse fs ts
    9.12 +  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
    9.13  
    9.14 -    and f (t as Type (_, ars)) = p t orelse fs ars
    9.15 -      | f t = p t;
    9.16 -  in f end;
    9.17 -
    9.18 -fun check_const p (nm, (ty, _)) =
    9.19 -  if p (nm, ty)
    9.20 -  then SOME (Term.size_of_typ ty)
    9.21 -  else NONE;
    9.22 +fun check_const pred (nm, (ty, _)) =
    9.23 +  if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
    9.24  
    9.25  fun opt_not f (c as (_, (ty, _))) =
    9.26 -  if is_some (f c)
    9.27 -  then NONE else SOME (Term.size_of_typ ty);
    9.28 +  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
    9.29  
    9.30  fun filter_const _ NONE = NONE
    9.31    | filter_const f (SOME (c, r)) =
    9.32 @@ -71,8 +60,7 @@
    9.33      val ty' = Logic.unvarifyT_global ty;
    9.34    in
    9.35      Pretty.block
    9.36 -     [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    9.37 -      Pretty.str "::", Pretty.brk 1,
    9.38 +     [Pretty.str nm, Pretty.str " ::", Pretty.brk 1,
    9.39        Pretty.quote (Syntax.pretty_typ ctxt ty')]
    9.40    end;
    9.41  
    9.42 @@ -128,35 +116,35 @@
    9.43  
    9.44      val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
    9.45    in
    9.46 -    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
    9.47 -      :: Pretty.str ""
    9.48 -      :: (Pretty.str o implode)
    9.49 -           (if null matches
    9.50 -            then ["nothing found", end_msg]
    9.51 -            else ["found ", (string_of_int o length) matches,
    9.52 -                  " constants", end_msg, ":"])
    9.53 -      :: Pretty.str ""
    9.54 -      :: map (pretty_const ctxt) matches
    9.55 -    |> Pretty.chunks
    9.56 -    |> Pretty.writeln
    9.57 -  end;
    9.58 +    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
    9.59 +    Pretty.str "" ::
    9.60 +    Pretty.str
    9.61 +     (if null matches
    9.62 +      then "nothing found" ^ end_msg
    9.63 +      else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
    9.64 +    Pretty.str "" ::
    9.65 +    map (pretty_const ctxt) matches
    9.66 +  end |> Pretty.chunks |> Pretty.writeln;
    9.67  
    9.68  
    9.69  (* command syntax *)
    9.70  
    9.71 -fun find_consts_cmd spec =
    9.72 -  Toplevel.unknown_theory o Toplevel.keep (fn state =>
    9.73 -    find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
    9.74 +local
    9.75  
    9.76  val criterion =
    9.77    Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
    9.78    Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
    9.79    Parse.xname >> Loose;
    9.80  
    9.81 +in
    9.82 +
    9.83  val _ =
    9.84    Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
    9.85      (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
    9.86 -      >> (Toplevel.no_timing oo find_consts_cmd));
    9.87 +      >> (fn spec => Toplevel.no_timing o
    9.88 +        Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
    9.89  
    9.90  end;
    9.91  
    9.92 +end;
    9.93 +
    10.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Aug 11 14:45:38 2010 +0200
    10.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Aug 11 18:17:53 2010 +0200
    10.3 @@ -433,36 +433,27 @@
    10.4  
    10.5      val tally_msg =
    10.6        (case foundo of
    10.7 -        NONE => "displaying " ^ string_of_int returned ^ " theorems"
    10.8 +        NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
    10.9        | SOME found =>
   10.10 -          "found " ^ string_of_int found ^ " theorems" ^
   10.11 +          "found " ^ string_of_int found ^ " theorem(s)" ^
   10.12              (if returned < found
   10.13               then " (" ^ string_of_int returned ^ " displayed)"
   10.14               else ""));
   10.15  
   10.16      val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   10.17    in
   10.18 -    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
   10.19 -        :: Pretty.str "" ::
   10.20 -     (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
   10.21 -      else
   10.22 -        [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
   10.23 +    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
   10.24 +    Pretty.str "" ::
   10.25 +    (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
   10.26 +     else
   10.27 +      [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
   10.28          map (pretty_thm ctxt) thms)
   10.29 -    |> Pretty.chunks |> Pretty.writeln
   10.30 -  end;
   10.31 +  end |> Pretty.chunks |> Pretty.writeln;
   10.32  
   10.33  
   10.34  
   10.35  (** command syntax **)
   10.36  
   10.37 -fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
   10.38 -  Toplevel.unknown_theory o Toplevel.keep (fn state =>
   10.39 -    let
   10.40 -      val proof_state = Toplevel.enter_proof_body state;
   10.41 -      val ctxt = Proof.context_of proof_state;
   10.42 -      val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
   10.43 -    in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
   10.44 -
   10.45  local
   10.46  
   10.47  val criterion =
   10.48 @@ -486,7 +477,13 @@
   10.49    Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
   10.50      Keyword.diag
   10.51      (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
   10.52 -      >> (Toplevel.no_timing oo find_theorems_cmd));
   10.53 +      >> (fn ((opt_lim, rem_dups), spec) =>
   10.54 +        Toplevel.no_timing o
   10.55 +        Toplevel.keep (fn state =>
   10.56 +          let
   10.57 +            val ctxt = Toplevel.context_of state;
   10.58 +            val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
   10.59 +          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
   10.60  
   10.61  end;
   10.62  
    11.1 --- a/src/Pure/codegen.ML	Wed Aug 11 14:45:38 2010 +0200
    11.2 +++ b/src/Pure/codegen.ML	Wed Aug 11 18:17:53 2010 +0200
    11.3 @@ -889,9 +889,8 @@
    11.4                mk_app false (str "testf") (map (str o fst) args),
    11.5                Pretty.brk 1, str "then NONE",
    11.6                Pretty.brk 1, str "else ",
    11.7 -              Pretty.block [str "SOME ", Pretty.block (str "[" ::
    11.8 -                Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
    11.9 -                  [str "]"])]]),
   11.10 +              Pretty.block [str "SOME ",
   11.11 +                Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
   11.12            str ");"]) ^
   11.13        "\n\nend;\n";
   11.14      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;