1.1 --- a/src/Pure/Proof/proof_syntax.ML Wed May 19 09:21:30 2010 +0200
1.2 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jun 01 10:46:47 2010 +0200
1.3 @@ -11,8 +11,9 @@
1.4 val proof_of_term: theory -> bool -> term -> Proofterm.proof
1.5 val term_of_proof: Proofterm.proof -> term
1.6 val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
1.7 - val read_term: theory -> typ -> string -> term
1.8 - val read_proof: theory -> bool -> string -> Proofterm.proof
1.9 + val strip_sorts_consttypes: Proof.context -> Proof.context
1.10 + val read_term: theory -> bool -> typ -> string -> term
1.11 + val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
1.12 val proof_syntax: Proofterm.proof -> theory -> theory
1.13 val proof_of: bool -> thm -> Proofterm.proof
1.14 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
1.15 @@ -109,7 +110,7 @@
1.16 | "thm" :: xs =>
1.17 let val name = Long_Name.implode xs;
1.18 in (case AList.lookup (op =) thms name of
1.19 - SOME thm => fst (strip_combt (Thm.proof_of thm))
1.20 + SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm))))
1.21 | NONE => error ("Unknown theorem " ^ quote name))
1.22 end
1.23 | _ => error ("Illegal proof constant name: " ^ quote s))
1.24 @@ -198,7 +199,14 @@
1.25 (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
1.26 end;
1.27
1.28 -fun read_term thy =
1.29 +fun strip_sorts_consttypes ctxt =
1.30 + let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt)
1.31 + in Symtab.fold (fn (s, (T, _)) =>
1.32 + ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T)))
1.33 + tab ctxt
1.34 + end;
1.35 +
1.36 +fun read_term thy topsort =
1.37 let
1.38 val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
1.39 val axm_names = map fst (Theory.all_axioms_of thy);
1.40 @@ -208,15 +216,19 @@
1.41 (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
1.42 |> ProofContext.init_global
1.43 |> ProofContext.allow_dummies
1.44 - |> ProofContext.set_mode ProofContext.mode_schematic;
1.45 + |> ProofContext.set_mode ProofContext.mode_schematic
1.46 + |> (if topsort then
1.47 + strip_sorts_consttypes #>
1.48 + ProofContext.set_defsort []
1.49 + else I);
1.50 in
1.51 fn ty => fn s =>
1.52 (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
1.53 |> TypeInfer.constrain ty |> Syntax.check_term ctxt
1.54 end;
1.55
1.56 -fun read_proof thy =
1.57 - let val rd = read_term thy proofT
1.58 +fun read_proof thy topsort =
1.59 + let val rd = read_term thy topsort proofT
1.60 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
1.61
1.62 fun proof_syntax prf =