# HG changeset patch
# User ballarin
# Date 1227532984 -3600
# Node ID 9ff624bd4fe1b5effee6fb74a105fedade61a422
# Parent  a87d27cc8498c92be7a972684f33717d4553c407
More ramifications of removal of 'includes' element.

diff -r a87d27cc8498 -r 9ff624bd4fe1 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Nov 23 18:37:56 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Nov 24 14:23:04 2008 +0100
@@ -262,8 +262,8 @@
   (case concl of
     Element.Shows shows =>
       let
-        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
-        val prems = subtract_prems loc_ctxt elems_ctxt;
+        val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
+        val prems = subtract_prems ctxt elems_ctxt;
         val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
         val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
       in ((prems, stmt, []), goal_ctxt) end
@@ -277,7 +277,7 @@
             (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
-        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
+        val (_, _, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
 
         val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
 
@@ -300,7 +300,7 @@
 
         val atts = map (Attrib.internal o K)
           [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
-        val prems = subtract_prems loc_ctxt elems_ctxt;
+        val prems = subtract_prems ctxt elems_ctxt;
         val stmt = [((Name.no_binding, atts), [(thesis, [])])];
 
         val (facts, goal_ctxt) = elems_ctxt