modernized strcture Proof_Checker;
authorwenzelm
Mon Aug 08 16:38:59 2011 +0200 (2011-08-08)
changeset 44057fda143b5c2f5
parent 44056 be825a69fc67
child 44058 ae85c5d64913
modernized strcture Proof_Checker;
src/Pure/Proof/extraction.ML
src/Pure/Proof/proofchecker.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Aug 08 16:09:34 2011 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Aug 08 16:38:59 2011 +0200
     1.3 @@ -795,7 +795,7 @@
     1.4               |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
     1.5                    Thm.varifyT_global (funpow (length (vars_of corr_prop))
     1.6                      (Thm.forall_elim_var 0) (Thm.forall_intr_frees
     1.7 -                      (ProofChecker.thm_of_proof thy'
     1.8 +                      (Proof_Checker.thm_of_proof thy'
     1.9                         (fst (Proofterm.freeze_thaw_prf prf))))))
    1.10               |> snd
    1.11               |> fold Code.add_default_eqn def_thms
     2.1 --- a/src/Pure/Proof/proofchecker.ML	Mon Aug 08 16:09:34 2011 +0200
     2.2 +++ b/src/Pure/Proof/proofchecker.ML	Mon Aug 08 16:38:59 2011 +0200
     2.3 @@ -10,17 +10,17 @@
     2.4    val thm_of_proof : theory -> Proofterm.proof -> thm
     2.5  end;
     2.6  
     2.7 -structure ProofChecker : PROOF_CHECKER =
     2.8 +structure Proof_Checker : PROOF_CHECKER =
     2.9  struct
    2.10  
    2.11  (***** construct a theorem out of a proof term *****)
    2.12  
    2.13  fun lookup_thm thy =
    2.14 -  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
    2.15 -  in
    2.16 -    (fn s => case Symtab.lookup tab s of
    2.17 -       NONE => error ("Unknown theorem " ^ quote s)
    2.18 -     | SOME thm => thm)
    2.19 +  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
    2.20 +    fn s =>
    2.21 +      (case Symtab.lookup tab s of
    2.22 +        NONE => error ("Unknown theorem " ^ quote s)
    2.23 +      | SOME thm => thm)
    2.24    end;
    2.25  
    2.26  val beta_eta_convert =
    2.27 @@ -87,10 +87,12 @@
    2.28            let
    2.29              val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
    2.30              val {prop, ...} = rep_thm thm;
    2.31 -            val _ = if is_equal prop prop' then () else
    2.32 -              error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    2.33 -                Syntax.string_of_term_global thy prop ^ "\n\n" ^
    2.34 -                Syntax.string_of_term_global thy prop');
    2.35 +            val _ =
    2.36 +              if is_equal prop prop' then ()
    2.37 +              else
    2.38 +                error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    2.39 +                  Syntax.string_of_term_global thy prop ^ "\n\n" ^
    2.40 +                  Syntax.string_of_term_global thy prop');
    2.41            in thm_of_atom thm Ts end
    2.42  
    2.43        | thm_of _ _ (PAxm (name, _, SOME Ts)) =