# HG changeset patch
# User wenzelm
# Date 1177353852 -7200
# Node ID 9bb135fa520611763546f8a371dad42350790c97
# Parent  e0788ff2e8117bbc7514772920a275947f3719aa
sane version of read_termTs (proper freeze);
added read_terms, cert_terms;

diff -r e0788ff2e811 -r 9bb135fa5206 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Apr 23 20:44:11 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 23 20:44:12 2007 +0200
@@ -51,9 +51,6 @@
   val revert_skolem: Proof.context -> string -> string
   val revert_skolems: Proof.context -> term -> term
   val decode_term: Proof.context -> term -> term
-  val read_termTs: Proof.context -> (string -> bool) -> (indexname -> typ option)
-    -> (indexname -> sort option) -> string list -> (string * typ) list
-    -> term list * (indexname * typ) list
   val read_termTs_schematic: Proof.context -> (string -> bool) -> (indexname -> typ option)
     -> (indexname -> sort option) -> string list -> (string * typ) list
     -> term list * (indexname * typ) list
@@ -61,10 +58,13 @@
   val read_term: Proof.context -> string -> term
   val read_prop: Proof.context -> string -> term
   val read_prop_schematic: Proof.context -> string -> term
+  val read_termTs: Proof.context -> (string * typ) list -> term list
+  val read_terms: Proof.context -> string 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
@@ -438,7 +438,7 @@
   #1 (read_def_termT freeze pp syn thy defaults fixed (s, propT));
 
 fun read_terms_thy freeze pp syn thy defaults fixed =
-  #1 o read_def_termTs freeze pp syn thy defaults fixed o map (rpair dummyT);
+  #1 o read_def_termTs freeze pp syn thy defaults fixed;
 
 fun read_props_thy freeze pp syn thy defaults fixed =
   #1 o read_def_termTs freeze pp syn thy defaults fixed o map (rpair propT);
@@ -532,7 +532,6 @@
 
 in
 
-val read_termTs           = gen_read' (read_def_termTs false) (apfst o map) false false;
 val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false true;
 
 fun read_term_pats T ctxt =
@@ -545,7 +544,8 @@
 val read_term            = gen_read (read_term_thy true) I false false;
 val read_prop            = gen_read (read_prop_thy true) I false false;
 val read_prop_schematic  = gen_read (read_prop_thy true) I false true;
-val read_terms           = gen_read (read_terms_thy true) map false false;
+val read_termTs          = gen_read (read_terms_thy true) map false false;
+fun read_terms ctxt      = read_termTs ctxt o map (rpair dummyT);
 fun read_props schematic = gen_read (read_props_thy true) map false schematic;
 
 end;
@@ -565,6 +565,7 @@
 in
 
 val cert_term = gen_cert false false false;
+val cert_terms = map o cert_term;
 val cert_prop = gen_cert true false false;
 val cert_props = map oo gen_cert true false;
 
@@ -695,7 +696,7 @@
 in
 
 val match_bind = gen_binds read_terms read_term_pats;
-val match_bind_i = gen_binds (map o cert_term) cert_term_pats;
+val match_bind_i = gen_binds cert_terms cert_term_pats;
 
 end;