src/Pure/Isar/proof.ML
changeset 15570 8d8c70b41bab
parent 15533 accd51fdae3c
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -269,7 +269,7 @@
     1.4  val reset_facts = put_facts NONE;
     1.5  
     1.6  fun these_factss (state, named_factss) =
     1.7 -  state |> put_facts (SOME (flat (map snd named_factss)));
     1.8 +  state |> put_facts (SOME (List.concat (map snd named_factss)));
     1.9  
    1.10  
    1.11  (* goal *)
    1.12 @@ -414,7 +414,7 @@
    1.13  
    1.14      fun prt_names names =
    1.15        (case filter_out (equal "") names of [] => ""
    1.16 -      | nms => " " ^ enclose "(" ")" (space_implode " and " (take (7, nms) @
    1.17 +      | nms => " " ^ enclose "(" ")" (space_implode " and " (Library.take (7, nms) @
    1.18            (if length nms > 7 then ["..."] else []))));
    1.19  
    1.20      fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
    1.21 @@ -546,7 +546,7 @@
    1.22  
    1.23      val {hyps, sign, ...} = Thm.rep_thm raw_th;
    1.24      val tsig = Sign.tsig_of sign;
    1.25 -    val casms = flat (map #1 (ProofContext.assumptions_of (context_of state)));
    1.26 +    val casms = List.concat (map #1 (ProofContext.assumptions_of (context_of state)));
    1.27      val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
    1.28  
    1.29      val th = raw_th RS Drule.rev_triv_goal;
    1.30 @@ -626,7 +626,7 @@
    1.31    |> map_context_result (f (map (pair ("", [])) args))
    1.32    |> (fn (st, named_facts) =>
    1.33      let val (_, (_, ((result, (facts, thm)), x))) = find_goal st;
    1.34 -    in st |> map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), x)) end);
    1.35 +    in st |> map_goal I (K ((result, (facts @ List.concat (map snd named_facts), thm)), x)) end);
    1.36  
    1.37  in
    1.38  
    1.39 @@ -754,12 +754,12 @@
    1.40        |> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
    1.41      val sign' = sign_of state';
    1.42  
    1.43 -    val props = flat propss;
    1.44 +    val props = List.concat propss;
    1.45      val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
    1.46      val goal = Drule.mk_triv_goal cprop;
    1.47  
    1.48 -    val tvars = foldr Term.add_term_tvars (props, []);
    1.49 -    val vars = foldr Term.add_term_vars (props, []);
    1.50 +    val tvars = Library.foldr Term.add_term_tvars (props, []);
    1.51 +    val vars = Library.foldr Term.add_term_vars (props, []);
    1.52    in
    1.53      if null tvars then ()
    1.54      else raise STATE ("Goal statement contains illegal schematic type variable(s): " ^
    1.55 @@ -786,7 +786,7 @@
    1.56    let
    1.57      val init = init_state thy;
    1.58      val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
    1.59 -      prep (apsome fst raw_locale) elems (map snd concl) (context_of init);
    1.60 +      prep (Option.map fst raw_locale) elems (map snd concl) (context_of init);
    1.61    in
    1.62      init
    1.63      |> open_block
    1.64 @@ -798,7 +798,7 @@
    1.65      |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
    1.66        (Theorem {kind = kind,
    1.67          theory_spec = (a, map (snd o fst) concl),
    1.68 -        locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (the opt_name, x)),
    1.69 +        locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
    1.70          view = view})
    1.71        Seq.single true (map (fst o fst) concl) propp
    1.72    end;
    1.73 @@ -863,7 +863,7 @@
    1.74      val outer_state = state |> close_block;
    1.75      val outer_ctxt = context_of outer_state;
    1.76  
    1.77 -    val ts = flat tss;
    1.78 +    val ts = List.concat tss;
    1.79      val results = prep_result state ts raw_thm;
    1.80      val resultq =
    1.81        results |> map (ProofContext.export false goal_ctxt outer_ctxt)
    1.82 @@ -903,7 +903,7 @@
    1.83      val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view)} =
    1.84        (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
    1.85  
    1.86 -    val ts = flat tss;
    1.87 +    val ts = List.concat tss;
    1.88      val locale_results = map (ProofContext.export_standard elems_view goal_ctxt locale_ctxt)
    1.89        (prep_result state ts raw_thm);
    1.90  
    1.91 @@ -920,12 +920,12 @@
    1.92            |> (fn ((thy', ctxt'), res) =>
    1.93              if name = "" andalso null loc_atts then thy'
    1.94              else (thy', ctxt')
    1.95 -              |> (#1 o #1 o Locale.add_thmss loc [((name, flat (map #2 res)), loc_atts)])))
    1.96 +              |> (#1 o #1 o Locale.add_thmss loc [((name, List.concat (map #2 res)), loc_atts)])))
    1.97        |> Locale.smart_note_thmss k locale_spec
    1.98          ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
    1.99        |> (fn (thy, res) => (thy, res)
   1.100            |>> (#1 o Locale.smart_note_thmss k locale_spec
   1.101 -            [((name, atts), [(flat (map #2 res), [])])]));
   1.102 +            [((name, atts), [(List.concat (map #2 res), [])])]));
   1.103    in (theory', ((k, name), results')) end;
   1.104  
   1.105