Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorChristian Urban <urbanc@in.tum.de>
Wed, 22 Jun 2011 14:14:54 +0100
changeset 2887 4e04f38329e5
parent 2886 d7066575cbb9
child 2888 eda5aeb056a6
tuned
Nominal/Nominal2.thy file | annotate | diff | comparison | revisions
Nominal/nominal_library.ML file | annotate | diff | comparison | revisions 
--- a/Nominal/Nominal2.thy	Wed Jun 22 13:40:25 2011 +0100
+++ b/Nominal/Nominal2.thy	Wed Jun 22 14:14:54 2011 +0100
@@ -189,23 +189,21 @@
   val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) =
     define_raw_dts dts bn_funs bn_eqs bclauses lthy   
 
-  val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
-  val {descr, sorts, ...} = dtinfo
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names 
+  val {descr, sorts, ...} = hd dtinfos
 
-  val raw_tys = all_dtyps descr sorts
+  val raw_tys = Datatype_Aux.get_rec_types descr sorts
   val tvs = hd raw_tys
     |> snd o dest_Type
     |> map dest_TFree  
 
-  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names  
- 
   val raw_cns_info = all_dtyp_constrs_types descr sorts
   val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info
 
   val raw_inject_thms = flat (map #inject dtinfos)
   val raw_distinct_thms = flat (map #distinct dtinfos)
-  val raw_induct_thm = #induct dtinfo
-  val raw_induct_thms = #inducts dtinfo
+  val raw_induct_thm = #induct (hd dtinfos)
+  val raw_induct_thms = #inducts (hd dtinfos)
   val raw_exhaust_thms = map #exhaust dtinfos
   val raw_size_trms = map HOLogic.size_const raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
--- a/Nominal/nominal_library.ML	Wed Jun 22 13:40:25 2011 +0100
+++ b/Nominal/nominal_library.ML	Wed Jun 22 14:14:54 2011 +0100
@@ -80,7 +80,6 @@
   (* datatype operations *)
   type cns_info = (term * typ * typ list * bool list) list
 
-  val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list
 
   (* tactics for function package *)
@@ -310,10 +309,6 @@
     - flags indicating whether the argument is recursive
 *)
 
-(* returns the type of the nth datatype *)
-fun all_dtyps descr sorts = 
-  map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))
-
 (* returns info about constructors in a datatype *)
 fun all_dtyp_constrs_info descr = 
   map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr
nominal2