equal
deleted
inserted
replaced
24 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; |
24 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; |
25 |
25 |
26 |
26 |
27 fun simple_read_term thy T s = |
27 fun simple_read_term thy T s = |
28 let |
28 let |
29 val ctxt = ProofContext.init_global thy |
29 val ctxt = Proof_Context.init_global thy |
30 |> ProofContext.allow_dummies |
30 |> Proof_Context.allow_dummies |
31 |> ProofContext.set_mode ProofContext.mode_schematic; |
31 |> Proof_Context.set_mode Proof_Context.mode_schematic; |
32 val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; |
32 val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; |
33 in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end; |
33 in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end; |
34 |
34 |
35 |
35 |
36 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
36 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |