src/HOL/Nominal/nominal_package.ML
changeset 18246 676d2e625d98
parent 18245 65e60434b3c2
child 18261 1318955d57ac
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Nov 25 14:00:22 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Nov 25 14:51:39 2005 +0100
     1.3 @@ -997,11 +997,15 @@
     1.4  
     1.5      (**** prove that new datatypes have finite support ****)
     1.6  
     1.7 +    val _ = warning "proving finite support for the new datatype";
     1.8 +
     1.9      val indnames = DatatypeProp.make_tnames recTs;
    1.10  
    1.11      val abs_supp = PureThy.get_thms thy8 (Name "abs_supp");
    1.12      val supp_atm = PureThy.get_thms thy8 (Name "supp_atm");
    1.13  
    1.14 +
    1.15 +(*
    1.16      val finite_supp_thms = map (fn atom =>
    1.17        let val atomT = Type (atom, [])
    1.18        in map standard (List.take
    1.19 @@ -1017,6 +1021,7 @@
    1.20                 List.concat supp_thms))))),
    1.21           length new_type_names))
    1.22        end) atoms;
    1.23 +*)
    1.24  
    1.25      (**** strong induction theorem ****)
    1.26  
    1.27 @@ -1081,13 +1086,13 @@
    1.28        DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
    1.29        DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
    1.30        DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms |>>
    1.31 -      fold (fn (atom, ths) => fn thy =>
    1.32 +  (*    fold (fn (atom, ths) => fn thy =>
    1.33          let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
    1.34          in fold (fn T => AxClass.add_inst_arity_i
    1.35              (fst (dest_Type T),
    1.36                replicate (length sorts) [class], [class])
    1.37              (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    1.38 -        end) (atoms ~~ finite_supp_thms) |>>
    1.39 +        end) (atoms ~~ finite_supp_thms) |>> *)
    1.40        Theory.add_path big_name |>>>
    1.41        PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] |>>
    1.42        Theory.parent_path;