src/Pure/Isar/specification.ML
changeset 21435 883337ea2f3b
parent 21370 d9dd7b4e5e69
child 21450 f16c9e6401d1
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 21 18:07:30 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 21 18:07:31 2006 +0100
     1.3 @@ -102,7 +102,7 @@
     1.4      val ((consts, axioms), lthy') = lthy
     1.5        |> LocalTheory.consts spec_frees vars
     1.6        ||> fold (fold Variable.auto_fixes o snd) specs   (* FIXME !? *)
     1.7 -      ||>> LocalTheory.axioms specs;
     1.8 +      ||>> LocalTheory.axioms Thm.axiomK specs;
     1.9  
    1.10      (* FIXME generic target!? *)
    1.11      val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) consts;
    1.12 @@ -130,9 +130,9 @@
    1.13            else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
    1.14          val ((lhs, (_, th)), lthy2) = lthy1
    1.15  (*          |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
    1.16 -          |> LocalTheory.def ((x, mx), ((name, []), rhs));
    1.17 +          |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
    1.18          val ((b, [th']), lthy3) = lthy2
    1.19 -          |> LocalTheory.note ((name, atts), [prove lthy2 th]);
    1.20 +          |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]);
    1.21        in (((x, T), (lhs, (b, th'))), LocalTheory.restore lthy3) end;
    1.22  
    1.23      val ((cs, defs), lthy') = lthy |> fold_map define args |>> split_list;
    1.24 @@ -185,12 +185,11 @@
    1.25  
    1.26  fun gen_theorems prep_thms prep_att kind raw_facts lthy =
    1.27    let
    1.28 -    val k = if kind = "" then [] else [Attrib.kind kind];
    1.29      val attrib = prep_att (ProofContext.theory_of lthy);
    1.30      val facts = raw_facts |> map (fn ((name, atts), bs) =>
    1.31        ((name, map attrib atts),
    1.32 -        bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts @ k))));
    1.33 -    val (res, lthy') = lthy |> LocalTheory.notes facts;
    1.34 +        bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
    1.35 +    val (res, lthy') = lthy |> LocalTheory.notes kind facts;
    1.36      val _ = present_results' lthy' kind res;
    1.37    in (res, lthy') end;
    1.38  
    1.39 @@ -246,8 +245,8 @@
    1.40          val (facts, goal_ctxt) = elems_ctxt
    1.41            |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
    1.42            |> fold_map assume_case (obtains ~~ propp)
    1.43 -          |-> (fn ths =>
    1.44 -            ProofContext.note_thmss_i [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
    1.45 +          |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
    1.46 +                [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
    1.47        in ((stmt, facts), goal_ctxt) end);
    1.48  
    1.49  fun gen_theorem prep_att prep_stmt
    1.50 @@ -255,7 +254,6 @@
    1.51    let
    1.52      val _ = LocalTheory.assert lthy0;
    1.53      val thy = ProofContext.theory_of lthy0;
    1.54 -    val attrib = prep_att thy;
    1.55  
    1.56      val (loc, ctxt, lthy) =
    1.57        (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
    1.58 @@ -263,28 +261,26 @@
    1.59            (SOME loc, ProofContext.init thy, LocalTheory.restore lthy0)
    1.60        | _ => (NONE, lthy0, lthy0));
    1.61  
    1.62 +    val attrib = prep_att thy;
    1.63 +    val atts = map attrib raw_atts;
    1.64 +
    1.65      val elems = raw_elems |> (map o Locale.map_elem)
    1.66        (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib});
    1.67      val ((stmt, facts), goal_ctxt) = prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
    1.68  
    1.69 -    val k = if kind = "" then [] else [Attrib.kind kind];
    1.70 -    val names = map (fst o fst) stmt;
    1.71 -    val attss = map (fn ((_, atts), _) => atts @ k) stmt;
    1.72 -    val atts = map attrib raw_atts @ k;
    1.73 -
    1.74      fun after_qed' results goal_ctxt' =
    1.75        let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in
    1.76          lthy
    1.77 -        |> LocalTheory.notes ((names ~~ attss) ~~ map (fn ths => [(ths, [])]) results')
    1.78 +        |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    1.79          |> (fn (res, lthy') =>
    1.80            (present_results lthy' ((kind, name), res);
    1.81 -            if name = "" andalso null raw_atts then lthy'
    1.82 -            else #2 (LocalTheory.notes [((name, atts), [(maps #2 res, [])])] lthy')))
    1.83 +            if name = "" andalso null atts then lthy'
    1.84 +            else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
    1.85          |> after_qed results'
    1.86        end;
    1.87    in
    1.88      goal_ctxt
    1.89 -    |> Proof.theorem_i kind before_qed after_qed' (map snd stmt)
    1.90 +    |> Proof.theorem_i before_qed after_qed' (map snd stmt)
    1.91      |> Proof.refine_insert facts
    1.92    end;
    1.93