src/Pure/Isar/specification.ML
changeset 28877 9ff624bd4fe1
parent 28862 53f13f763d4f
child 28880 f6a547c5dbbf
     1.1 --- a/src/Pure/Isar/specification.ML	Sun Nov 23 18:37:56 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Mon Nov 24 14:23:04 2008 +0100
     1.3 @@ -262,8 +262,8 @@
     1.4    (case concl of
     1.5      Element.Shows shows =>
     1.6        let
     1.7 -        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
     1.8 -        val prems = subtract_prems loc_ctxt elems_ctxt;
     1.9 +        val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
    1.10 +        val prems = subtract_prems ctxt elems_ctxt;
    1.11          val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
    1.12          val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
    1.13        in ((prems, stmt, []), goal_ctxt) end
    1.14 @@ -277,7 +277,7 @@
    1.15              (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
    1.16  
    1.17          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    1.18 -        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
    1.19 +        val (_, _, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
    1.20  
    1.21          val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
    1.22  
    1.23 @@ -300,7 +300,7 @@
    1.24  
    1.25          val atts = map (Attrib.internal o K)
    1.26            [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
    1.27 -        val prems = subtract_prems loc_ctxt elems_ctxt;
    1.28 +        val prems = subtract_prems ctxt elems_ctxt;
    1.29          val stmt = [((Name.no_binding, atts), [(thesis, [])])];
    1.30  
    1.31          val (facts, goal_ctxt) = elems_ctxt