# HG changeset patch
# User wenzelm
# Date 1232573209 -3600
# Node ID 0e1723e91ef8cbd88e0cfb942aded4b538c7b01b
# Parent  b660ee46f2f665892ffe86b5a8ba1bf97e852275
eliminated obsolete var morphism;
tuned;

diff -r b660ee46f2f6 -r 0e1723e91ef8 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Jan 21 22:26:48 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Jan 21 22:26:49 2009 +0100
@@ -198,11 +198,14 @@
 
 (** Parsing **)
 
-fun parse_elem prep_typ prep_term ctxt elem =
-  Element.map_ctxt' {binding = I, var = I, typ = prep_typ ctxt,
-  term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt), (* FIXME ?? *)
-  pat = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
-  fact = I, attrib = I} elem;
+fun parse_elem prep_typ prep_term ctxt =
+  Element.map_ctxt
+   {binding = I,
+    typ = prep_typ ctxt,
+    term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt),
+    pattern = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
+    fact = I,
+    attrib = I};
 
 fun parse_concl prep_term ctxt concl =
   (map o map) (fn (t, ps) =>
@@ -490,8 +493,7 @@
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
-    val export' =
-      Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+    val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   in ((propss, deps, export'), goal_ctxt) end;
     
 in