# HG changeset patch
# User wenzelm
# Date 1190579015 -7200
# Node ID 80da599dea376fc619f56d563e0d9dbe7667e308
# Parent  c62320337a4e6867465081dab20c68216bce27c7
added read_term_pattern/schematic/abbrev;
prepare_patterns: Variable.polymorphic;
removed obsolete cert/pats versions;

diff -r c62320337a4e -r 80da599dea37 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Sep 23 22:23:34 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 23 22:23:35 2007 +0200
@@ -58,19 +58,16 @@
   val revert_skolem: Proof.context -> string -> string
   val revert_skolems: Proof.context -> term -> term
   val decode_term: Proof.context -> term -> term
+  val read_term_pattern: Proof.context -> string -> term
+  val read_term_schematic: Proof.context -> string -> term
+  val read_term_abbrev: Proof.context -> string -> term
   val read_termTs_schematic: Proof.context -> (string -> bool) -> (indexname -> typ option)
     -> (indexname -> sort option) -> string list -> (string * typ) list
     -> term list * (indexname * typ) list
   val read_prop_legacy: Proof.context -> string -> term
   val read_termTs: Proof.context -> (string * typ) list -> term list
-  val read_term_pats: typ -> Proof.context -> string list -> term list
-  val read_prop_pats: Proof.context -> string list -> term list
-  val read_term_abbrev: Proof.context -> string -> term
   val cert_term: Proof.context -> term -> term
-  val cert_terms: Proof.context -> term list -> term list
   val cert_prop: Proof.context -> term -> term
-  val cert_term_pats: typ -> Proof.context -> term list -> term list
-  val cert_prop_pats: Proof.context -> term list -> term list
   val infer_type: Proof.context -> string -> typ
   val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
@@ -428,6 +425,15 @@
 
 (** prepare terms and propositions **)
 
+(* read_term *)
+
+fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
+
+val read_term_pattern   = read_term_mode mode_pattern;
+val read_term_schematic = read_term_mode mode_schematic;
+val read_term_abbrev    = read_term_mode mode_abbrev;
+
+
 (* read wrt. theory *)     (*exception ERROR*)
 
 fun read_def_termTs freeze pp syn ctxt (types, sorts, used) fixed sTs =
@@ -505,10 +511,11 @@
 
 in
 
-fun prepare_pattern ctxt =
+fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
-    Term.map_types (prepare_patternT ctxt) #>
-    (if pattern then prepare_dummies else reject_dummies)
+    (if pattern then Variable.polymorphic ctxt else I) #>
+    (map o Term.map_types) (prepare_patternT ctxt) #>
+    map (if pattern then prepare_dummies else reject_dummies)
   end;
 
 end;
@@ -562,7 +569,7 @@
         (legacy_intern_skolem ctxt internal types) s
       handle TERM (msg, _) => error msg)
     |> app (expand_abbrevs ctxt)
-    |> app (prepare_pattern ctxt)
+    |> app (singleton (prepare_patterns ctxt))
   end;
 
 fun gen_read read app pattern schematic ctxt =
@@ -572,10 +579,6 @@
 
 val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false true;
 
-fun read_term_pats T ctxt =
-  #1 o gen_read (read_def_termTs false) (apfst o map) true false ctxt o map (rpair T);
-val read_prop_pats = read_term_pats propT;
-
 fun read_prop_legacy ctxt =
   gen_read' (read_prop_thy true) I false false ctxt (K true) (K NONE) (K NONE) [];
 
@@ -589,24 +592,17 @@
 
 local
 
-fun gen_cert prop mode ctxt0 t =
-  let val ctxt = set_mode mode ctxt0 in
-    t
-    |> expand_abbrevs ctxt
-    |> (fn t' => #1 (Sign.certify' prop (pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
-      handle TYPE (msg, _, _) => error msg
-        | TERM (msg, _) => error msg)
-   end;
+fun gen_cert prop ctxt t =
+  t
+  |> expand_abbrevs ctxt
+  |> (fn t' => #1 (Sign.certify' prop (pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+    handle TYPE (msg, _, _) => error msg
+      | TERM (msg, _) => error msg);
 
 in
 
-val cert_term = gen_cert false mode_default;
-val cert_terms = map o cert_term;
-val cert_prop = gen_cert true mode_default;
-fun cert_props schematic = map o gen_cert true (if schematic then mode_schematic else mode_default);
-
-fun cert_term_pats _ = map o gen_cert false mode_pattern;
-val cert_prop_pats = map o gen_cert true mode_pattern;
+val cert_term = gen_cert false;
+val cert_prop = gen_cert true;
 
 end;
 
@@ -627,7 +623,7 @@
 fun standard_term_check ctxt =
   standard_infer_types ctxt #>
   map (expand_abbrevs ctxt) #>
-  map (prepare_pattern ctxt);
+  prepare_patterns ctxt;
 
 fun standard_typ_check ctxt =
   map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
@@ -691,8 +687,8 @@
 fun parse_term T ctxt str =
   let
     val thy = theory_of ctxt;
-    fun infer t = singleton (standard_infer_types (Type.set_mode Type.mode_default ctxt))
-        (TypeInfer.constrain t T);
+    val infer = singleton (standard_infer_types (Type.set_mode Type.mode_default ctxt)) o
+      TypeInfer.constrain T;
     fun check t = Exn.Result (infer t) handle ERROR msg => Exn.Exn (ERROR msg);
     val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
     val read = Syntax.standard_parse_term (pp ctxt) check get_sort map_const map_free map_type
@@ -760,18 +756,18 @@
 
 local
 
-fun prep_bind prep_pats (raw_pats, t) ctxt =
+fun gen_bind prep_terms gen raw_binds ctxt =
   let
-    val ctxt' = Variable.declare_term t ctxt;
-    val pats = prep_pats (Term.fastype_of t) ctxt' raw_pats;
-    val binds = simult_matches ctxt' (t, pats);
-  in (binds, ctxt') end;
+    fun prep_bind (raw_pats, t) ctxt1 =
+      let
+        val T = Term.fastype_of t;
+        val ctxt2 = Variable.declare_term t ctxt1;
+        val pats = prep_terms (set_mode mode_pattern ctxt2) T raw_pats;
+        val binds = simult_matches ctxt2 (t, pats);
+      in (binds, ctxt2) end;
 
-fun gen_binds prep_terms prep_pats gen raw_binds ctxt =
-  let
-    val ts = prep_terms (set_mode mode_default ctxt) (map snd raw_binds);
-    val (binds, ctxt') =
-      apfst flat (fold_map (prep_bind prep_pats) (map fst raw_binds ~~ ts) ctxt);
+    val ts = prep_terms ctxt dummyT (map #2 raw_binds);
+    val (binds, ctxt') = apfst flat (fold_map prep_bind (map #1 raw_binds ~~ ts) ctxt);
     val binds' =
       if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds)
       else binds;
@@ -785,8 +781,11 @@
 
 in
 
-val match_bind = gen_binds Syntax.read_terms read_term_pats;
-val match_bind_i = gen_binds cert_terms cert_term_pats;
+fun read_terms ctxt T =
+  map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
+
+val match_bind = gen_bind read_terms;
+val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
 
 end;
 
@@ -795,19 +794,19 @@
 
 local
 
-fun prep_propp schematic prep_props prep_pats (context, args) =
+fun prep_propp mode prep_props (context, args) =
   let
     fun prep (_, raw_pats) (ctxt, prop :: props) =
-          let val ctxt' = Variable.declare_term prop ctxt
-          in ((prop, prep_pats ctxt' raw_pats), (ctxt', props)) end
-      | prep _ _ = sys_error "prep_propp";
+      let val ctxt' = Variable.declare_term prop ctxt
+      in ((prop, prep_props (set_mode mode_pattern ctxt') raw_pats), (ctxt', props)) end;
+
     val (propp, (context', _)) = (fold_map o fold_map) prep args
-      (context, prep_props schematic context (maps (map fst) args));
+      (context, prep_props (set_mode mode context) (maps (map fst) args));
   in (context', propp) end;
 
-fun gen_bind_propp prepp (ctxt, raw_args) =
+fun gen_bind_propp mode parse_prop (ctxt, raw_args) =
   let
-    val (ctxt', args) = prepp (ctxt, raw_args);
+    val (ctxt', args) = prep_propp mode parse_prop (ctxt, raw_args);
     val binds = flat (flat (map (map (simult_matches ctxt')) args));
     val propss = map (map #1) args;
 
@@ -818,15 +817,15 @@
 
 in
 
-val read_propp = prep_propp false read_props read_prop_pats;
-val cert_propp = prep_propp false cert_props cert_prop_pats;
-val read_propp_schematic = prep_propp true read_props read_prop_pats;
-val cert_propp_schematic = prep_propp true cert_props cert_prop_pats;
+val read_propp           = prep_propp mode_default Syntax.read_props;
+val cert_propp           = prep_propp mode_default (map o cert_prop);
+val read_propp_schematic = prep_propp mode_schematic Syntax.read_props;
+val cert_propp_schematic = prep_propp mode_schematic (map o cert_prop);
 
-val bind_propp = gen_bind_propp read_propp;
-val bind_propp_i = gen_bind_propp cert_propp;
-val bind_propp_schematic = gen_bind_propp read_propp_schematic;
-val bind_propp_schematic_i = gen_bind_propp cert_propp_schematic;
+val bind_propp             = gen_bind_propp mode_default Syntax.read_props;
+val bind_propp_i           = gen_bind_propp mode_default (map o cert_prop);
+val bind_propp_schematic   = gen_bind_propp mode_schematic Syntax.read_props;
+val bind_propp_schematic_i = gen_bind_propp mode_schematic (map o cert_prop);
 
 end;
 
@@ -1027,8 +1026,6 @@
 
 (* abbreviations *)
 
-fun read_term_abbrev ctxt = Syntax.read_term (set_mode mode_abbrev ctxt);
-
 fun add_abbrev mode (c, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t