Use correct mode when parsing elements and conclusion.

--- a/src/Pure/Isar/element.ML	Sun Dec 14 15:43:04 2008 +0100
+++ b/src/Pure/Isar/element.ML	Tue Dec 16 12:08:10 2008 +0100
@@ -23,6 +23,10 @@
   val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
    (Attrib.binding * ('fact * Attrib.src list) list) list ->
    (Attrib.binding * ('c * Attrib.src list) list) list
+  val map_ctxt': {binding: Binding.T -> Binding.T,
+    var: Binding.T * mixfix -> Binding.T * mixfix,
+    typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c,
+    attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   val map_ctxt: {binding: Binding.T -> Binding.T,
     var: Binding.T * mixfix -> Binding.T * mixfix,
     typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
@@ -109,18 +113,22 @@
 
 fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
 
-fun map_ctxt {binding, var, typ, term, fact, attrib} =
+fun map_ctxt' {binding, var, typ, term, pat, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
        let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
        let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
-      ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
+      ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pat ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
-      ((binding a, map attrib atts), (term t, map term ps))))
+      ((binding a, map attrib atts), (term t, map pat ps))))
    | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
       ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
 
+fun map_ctxt {binding, var, typ, term, fact, attrib} =
+  map_ctxt' {binding = binding, var = var, typ = typ, term = term, pat = term,
+    fact = fact, attrib = attrib}
+
 fun map_ctxt_attrib attrib =
   map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
 

--- a/src/Pure/Isar/expression.ML	Sun Dec 14 15:43:04 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Dec 16 12:08:10 2008 +0100
@@ -184,12 +184,15 @@
 (** Parsing **)
 
 fun parse_elem prep_typ prep_term ctxt elem =
-  Element.map_ctxt {binding = I, var = I, typ = prep_typ ctxt,
-    term = prep_term ctxt, fact = I, attrib = I} 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_concl prep_term ctxt concl =
   (map o map) (fn (t, ps) =>
-    (prep_term ctxt, map (prep_term ctxt) ps)) concl;
+    (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t, (* FIXME ?? *)
+      map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
 
 
 (** Simultaneous type inference: instantiations + elements + conclusion **)
@@ -398,14 +401,12 @@
       let
         val ctxt' = declare_elem prep_vars raw_elem ctxt;
         val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
-        (* FIXME term bindings *)
         val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
       in (insts, elems', ctxt') end;
 
     fun prep_concl raw_concl (insts, elems, ctxt) =
       let
-        val concl = (map o map) (fn (t, ps) =>
-          (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl;
+        val concl = parse_concl parse_prop ctxt raw_concl;
       in check_autofix insts elems concl ctxt end;
 
     val fors = prep_vars fixed context |> fst;