# HG changeset patch
# User wenzelm
# Date 1190583582 -7200
# Node ID f24306b9e0731f33f4d96a05ab62ffb70a4edf8b
# Parent  8113d01493047455e98b110c50d81fd6b636cf2f
removed dead code;
tuned;

diff -r 8113d0149304 -r f24306b9e073 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Sep 23 23:00:01 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 23 23:39:42 2007 +0200
@@ -434,28 +434,6 @@
 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 =
-  Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt) fixed
-    ctxt (types, sorts) used freeze sTs;
-
-fun read_def_termT freeze pp syn ctxt defaults fixed sT =
-  apfst hd (read_def_termTs freeze pp syn ctxt defaults fixed [sT]);
-
-fun read_term_thy freeze pp syn thy defaults fixed s =
-  #1 (read_def_termT freeze pp syn thy defaults fixed (s, dummyT));
-
-fun read_prop_thy freeze pp syn thy defaults fixed s =
-  #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;
-
-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);
-
-
 (* local abbreviations *)
 
 local
@@ -551,17 +529,30 @@
   in Syntax.decode_term get_sort map_const map_free map_type map_sort end;
 
 
-(* read terms *)
+(* read terms -- legacy *)
 
 local
 
+fun read_def_termTs freeze pp syn ctxt (types, sorts, used) fixed sTs =
+  Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt) fixed
+    ctxt (types, sorts) used freeze sTs;
+
+fun read_def_termT freeze pp syn ctxt defaults fixed sT =
+  apfst hd (read_def_termTs freeze pp syn ctxt defaults fixed [sT]);
+
+fun read_prop_thy freeze pp syn thy defaults fixed s =
+  #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;
+
+
 fun append_env e1 e2 x = (case e2 x of NONE => e1 x | some => some);
 
-fun gen_read' read app pattern schematic ctxt0 internal more_types more_sorts more_used s =
+fun gen_read' read app schematic ctxt0 internal more_types more_sorts more_used s =
   let
-    val ctxt = ctxt0
-      |> set_mode (Mode {stmt = false, pattern = pattern, schematic = schematic, abbrev = false});
-    val types = append_env (Variable.def_type ctxt pattern) more_types;
+    val ctxt = if schematic then set_mode mode_schematic ctxt0 else ctxt0;
+    val types = append_env (Variable.def_type ctxt false) more_types;
     val sorts = append_env (Variable.def_sort ctxt) more_sorts;
     val used = fold Name.declare more_used (Variable.names_of ctxt);
   in
@@ -572,18 +563,17 @@
     |> app (singleton (prepare_patterns ctxt))
   end;
 
-fun gen_read read app pattern schematic ctxt =
-  gen_read' read app pattern schematic ctxt (K false) (K NONE) (K NONE) [];
+fun gen_read read app schematic ctxt =
+  gen_read' read app schematic ctxt (K false) (K NONE) (K NONE) [];
 
 in
 
-val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false true;
+val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) true;
 
 fun read_prop_legacy ctxt =
-  gen_read' (read_prop_thy true) I false false ctxt (K true) (K NONE) (K NONE) [];
+  gen_read' (read_prop_thy true) I false ctxt (K true) (K NONE) (K NONE) [];
 
-val read_termTs          = gen_read (read_terms_thy true) map false false;
-fun read_props schematic = gen_read (read_props_thy true) map false schematic;
+val read_termTs = gen_read (read_terms_thy true) map false;
 
 end;