src/Pure/Proof/proof_syntax.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -92,12 +92,12 @@
     1.4  fun disambiguate_names thy prf =
     1.5    let
     1.6      val thms = thms_of_proof Symtab.empty prf;
     1.7 -    val thms' = map (apsnd (#prop o rep_thm)) (flat
     1.8 +    val thms' = map (apsnd (#prop o rep_thm)) (List.concat
     1.9        (map PureThy.thms_of (thy :: Theory.ancestors_of thy)));
    1.10  
    1.11      val tab = Symtab.foldl (fn (tab, (key, ps)) =>
    1.12 -      let val prop = if_none (assoc (thms', key)) (Bound 0)
    1.13 -      in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
    1.14 +      let val prop = getOpt (assoc (thms', key), Bound 0)
    1.15 +      in fst (Library.foldr (fn ((prop', prf), x as (tab, i)) =>
    1.16          if prop <> prop' then
    1.17            (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
    1.18          else x) (ps, (tab, 1)))
    1.19 @@ -109,8 +109,8 @@
    1.20        | rename (prf % t) = rename prf % t
    1.21        | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
    1.22            let
    1.23 -            val prop' = if_none (assoc (thms', s)) (Bound 0);
    1.24 -            val ps = map fst (the (Symtab.lookup (thms, s))) \ prop'
    1.25 +            val prop' = getOpt (assoc (thms', s), Bound 0);
    1.26 +            val ps = map fst (valOf (Symtab.lookup (thms, s))) \ prop'
    1.27            in if prop = prop' then prf' else
    1.28              PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
    1.29                prf, prop, Ts)
    1.30 @@ -125,8 +125,8 @@
    1.31  fun proof_of_term thy tab ty =
    1.32    let
    1.33      val thys = thy :: Theory.ancestors_of thy;
    1.34 -    val thms = flat (map thms_of thys);
    1.35 -    val axms = flat (map (Symtab.dest o #axioms o rep_theory) thys);
    1.36 +    val thms = List.concat (map thms_of thys);
    1.37 +    val axms = List.concat (map (Symtab.dest o #axioms o rep_theory) thys);
    1.38  
    1.39      fun mk_term t = (if ty then I else map_term_types (K dummyT))
    1.40        (Term.no_dummy_patterns t);
    1.41 @@ -180,7 +180,7 @@
    1.42  val Oraclet = Const ("Oracle", propT --> proofT);
    1.43  val MinProoft = Const ("MinProof", proofT);
    1.44  
    1.45 -val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
    1.46 +val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt",
    1.47    [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
    1.48  
    1.49  fun term_of _ (PThm ((name, _), _, _, NONE)) =
    1.50 @@ -192,17 +192,17 @@
    1.51        mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
    1.52    | term_of _ (PBound i) = Bound i
    1.53    | term_of Ts (Abst (s, opT, prf)) = 
    1.54 -      let val T = if_none opT dummyT
    1.55 +      let val T = getOpt (opT,dummyT)
    1.56        in Const ("Abst", (T --> proofT) --> proofT) $
    1.57          Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
    1.58        end
    1.59    | term_of Ts (AbsP (s, t, prf)) =
    1.60 -      AbsPt $ if_none t (Const ("dummy_pattern", propT)) $
    1.61 +      AbsPt $ getOpt (t, Const ("dummy_pattern", propT)) $
    1.62          Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
    1.63    | term_of Ts (prf1 %% prf2) =
    1.64        AppPt $ term_of Ts prf1 $ term_of Ts prf2
    1.65    | term_of Ts (prf % opt) = 
    1.66 -      let val t = if_none opt (Const ("dummy_pattern", dummyT))
    1.67 +      let val t = getOpt (opt, Const ("dummy_pattern", dummyT))
    1.68        in Const ("Appt",
    1.69          [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
    1.70            term_of Ts prf $ t
    1.71 @@ -217,9 +217,9 @@
    1.72    let
    1.73      val (prf', tab) = disambiguate_names thy prf;
    1.74      val thys = thy :: Theory.ancestors_of thy;
    1.75 -    val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys))) @
    1.76 +    val thm_names = filter_out (equal "") (map fst (List.concat (map thms_of thys))) @
    1.77        map fst (Symtab.dest tab);
    1.78 -    val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
    1.79 +    val axm_names = map fst (List.concat (map (Symtab.dest o #axioms o rep_theory) thys));
    1.80      val sg = sign_of thy |>
    1.81        add_proof_syntax |>
    1.82        add_proof_atom_consts
    1.83 @@ -232,8 +232,8 @@
    1.84  fun read_term thy =
    1.85    let
    1.86      val thys = thy :: Theory.ancestors_of thy;
    1.87 -    val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys)));
    1.88 -    val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
    1.89 +    val thm_names = filter_out (equal "") (map fst (List.concat (map thms_of thys)));
    1.90 +    val axm_names = map fst (List.concat (map (Symtab.dest o #axioms o rep_theory) thys));
    1.91      val sg = sign_of thy |>
    1.92        add_proof_syntax |>
    1.93        add_proof_atom_consts