# HG changeset patch
# User wenzelm
# Date 928355344 -7200
# Node ID a9a515a43ae040a09a904d65053296ab9ddbe45a
# Parent  aa71a04f4b93ac7a52a83f611304694dae1aa6a8
read_term/prop_pat: do not freeze;

diff -r aa71a04f4b93 -r a9a515a43ae0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jun 02 22:27:01 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 02 22:29:04 1999 +0200
@@ -317,11 +317,11 @@
 fun read_def_termT freeze sg defs sT = apfst hd (read_def_termTs freeze sg defs [sT]);
 
 
-fun read_term_sg sg (defs as (_, _, used)) s =
-  #1 (read_def_termT true sg defs (s, TVar ((variant used "'z", 0), logicS)));
+fun read_term_sg freeze sg (defs as (_, _, used)) s =
+  #1 (read_def_termT freeze sg defs (s, TVar ((variant used "'z", 0), logicS)));
 
-fun read_prop_sg sg defs s =
-  #1 (read_def_termT true sg defs (s, propT));
+fun read_prop_sg freeze sg defs s =
+  #1 (read_def_termT freeze sg defs (s, propT));
 
 
 fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t);
@@ -389,18 +389,23 @@
 
 (* dummy patterns *)
 
+local
+
 fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN
   | is_dummy _ = false;
 
+fun prep_dummy (i, t) =
+  if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t);
+
+in
+
+fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
+
 fun reject_dummies ctxt tm =
   if foldl_aterms (fn (ok, t) => ok andalso not (is_dummy t)) (true, tm) then tm
   else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
 
-
-fun prep_dummy (i, t) =
-  if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t);
-
-fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
+end;
 
 
 (* read terms *)
@@ -425,10 +430,10 @@
   end;
 
 val read_termTs = gen_read (read_def_termTs false) (apfst o map) false;
-val read_term = gen_read read_term_sg I false;
-val read_prop = gen_read read_prop_sg I false;
-val read_term_pat = gen_read read_term_sg I true;
-val read_prop_pat = gen_read read_prop_sg I true;
+val read_term = gen_read (read_term_sg true) I false;
+val read_prop = gen_read (read_prop_sg true) I false;
+val read_term_pat = gen_read (read_term_sg false) I true;
+val read_prop_pat = gen_read (read_prop_sg false) I true;
 
 
 (* certify terms *)