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 =