src/Pure/Tools/class_package.ML
changeset 22209 86b688409dde
parent 22182 05ed4080cbd7
child 22222 bb07dd6cb1b9
equal deleted inserted replaced
22208:2d6e8cf48670 22209:86b688409dde
   465       name_locale
   465       name_locale
   466       |> Locale.global_asms_of thy
   466       |> Locale.global_asms_of thy
   467       |> map (NameSpace.base o fst o fst) (*FIXME*)
   467       |> map (NameSpace.base o fst o fst) (*FIXME*)
   468     fun mk_const thy class (c, ty) =
   468     fun mk_const thy class (c, ty) =
   469       Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty);
   469       Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty);
   470     (*fun note_thms class name_locale cs thy =
       
   471       let (*FIXME just an ad-hoc feature*)
       
   472         val names = fold (fn Element.Assumes xs => fold (cons o fst o fst) xs
       
   473           | Element.Notes (name, _) => cons name
       
   474           | _ => I) elems []
       
   475         val const_names = cs;
       
   476         val path = NameSpace.base class;
       
   477         val prefix = NameSpace.implode [class ^ "_class", space_implode "_" const_names];
       
   478         fun note_thm name thy =
       
   479           case try (PureThy.get_thm thy) (Name (NameSpace.append prefix name))
       
   480            of SOME thm =>
       
   481                 thy
       
   482                 |> PureThy.note_thmss_qualified "" path [((name, []), [([thm], [])])]
       
   483                 |> snd
       
   484             | NONE => error name;
       
   485       in
       
   486         thy
       
   487         |> fold note_thm names
       
   488       end;*)
       
   489   in
   470   in
   490     thy
   471     thy
   491     |> add_locale bname supexpr elems
   472     |> add_locale bname supexpr elems
   492     |-> (fn name_locale => ProofContext.theory_result (
   473     |-> (fn name_locale => ProofContext.theory_result (
   493       tap (fn thy => check_locale thy name_locale)
   474       tap (fn thy => check_locale thy name_locale)
   500         add_class_data ((name_axclass, supclasses),
   481         add_class_data ((name_axclass, supclasses),
   501           (name_locale, map (fst o fst) params ~~ map fst consts, axiom_names))
   482           (name_locale, map (fst o fst) params ~~ map fst consts, axiom_names))
   502       #> prove_interpretation (Logic.const_of_class bname, [])
   483       #> prove_interpretation (Logic.const_of_class bname, [])
   503           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
   484           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
   504             ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   485             ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   505       (*#> note_thms name_axclass name_locale (map fst supconsts @ map (fst o fst) params)*)
       
   506       #> pair name_axclass
   486       #> pair name_axclass
   507       )))))
   487       )))))
   508   end;
   488   end;
   509 
   489 
   510 in
   490 in