# HG changeset patch # User wenzelm # Date 1194809346 -3600 # Node ID 1aa7927a67590d58caf920d912f5953f344adcd3 # Parent 7ac8c93be6243b8b2052829068778936f46e13e6 simplified Consts.dest; export standard_infer_types; diff -r 7ac8c93be624 -r 1aa7927a6759 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Nov 11 20:29:05 2007 +0100 +++ b/src/Pure/Isar/proof_context.ML Sun Nov 11 20:29:06 2007 +0100 @@ -58,6 +58,7 @@ val read_const_proper: Proof.context -> string -> term val read_const: Proof.context -> string -> term val decode_term: Proof.context -> term -> term + val standard_infer_types: Proof.context -> term list -> term list val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term @@ -553,8 +554,6 @@ (* type checking/inference *) -local - fun standard_infer_types ctxt ts = let val Mode {pattern, ...} = get_mode ctxt in TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt) @@ -564,6 +563,8 @@ handle TYPE (msg, _, _) => error msg end; +local + fun standard_typ_check ctxt = map (cert_typ_mode (Type.get_mode ctxt) ctxt) #> map (prepare_patternT ctxt); @@ -1163,7 +1164,7 @@ val ((space, consts), (_, globals)) = pairself (#constants o Consts.dest) (#consts (rep_context ctxt)); fun add_abbr (_, (_, NONE)) = I - | add_abbr (c, (T, SOME (t, _))) = + | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t)); val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));