merged
authorwenzelm
Tue Aug 11 20:40:02 2009 +0200 (2009-08-11)
changeset 3236440d952bd6d47
parent 32363 a0ea6cd47724
parent 32361 141e5151b918
child 32365 9b74d0339c44
merged
     1.1 --- a/Admin/makedist	Mon Aug 10 13:53:42 2009 +0200
     1.2 +++ b/Admin/makedist	Tue Aug 11 20:40:02 2009 +0200
     1.3 @@ -165,8 +165,8 @@
     1.4  perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
     1.5  perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
     1.6  perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
     1.7 -perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
     1.8 -perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
     1.9 +perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
    1.10 +perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
    1.11  
    1.12  
    1.13  # create archives
     2.1 --- a/README	Mon Aug 10 13:53:42 2009 +0200
     2.2 +++ b/README	Tue Aug 11 20:40:02 2009 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  
     2.5  Version information
     2.6  
     2.7 -   This is the internal repository version of Isabelle.
     2.8 +   This is some unidentified repository version of Isabelle.
     2.9  
    2.10     See the NEWS file in the distribution for details on user-relevant
    2.11     changes.
     3.1 --- a/README_REPOSITORY	Mon Aug 10 13:53:42 2009 +0200
     3.2 +++ b/README_REPOSITORY	Tue Aug 11 20:40:02 2009 +0200
     3.3 @@ -208,8 +208,8 @@
     3.4      two-dimensional presentation too much.
     3.5  
     3.6  
     3.7 -Building Isabelle from the repository version
     3.8 ----------------------------------------------
     3.9 +Building a repository version of Isabelle
    3.10 +-----------------------------------------
    3.11  
    3.12  Compared to a proper distribution or development snapshot, a
    3.13  repository version of Isabelle lacks textual version identifiers in
     4.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex	Mon Aug 10 13:53:42 2009 +0200
     4.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 11 20:40:02 2009 +0200
     4.3 @@ -229,14 +229,14 @@
     4.4  \hspace*{0pt}module Example where {\char123}\\
     4.5  \hspace*{0pt}\\
     4.6  \hspace*{0pt}\\
     4.7 -\hspace*{0pt}foldla ::~forall a{\char95}1 b{\char95}1.~(a{\char95}1 -> b{\char95}1 -> a{\char95}1) -> a{\char95}1 -> [b{\char95}1] -> a{\char95}1;\\
     4.8 +\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
     4.9  \hspace*{0pt}foldla f a [] = a;\\
    4.10  \hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
    4.11  \hspace*{0pt}\\
    4.12  \hspace*{0pt}rev ::~forall a.~[a] -> [a];\\
    4.13  \hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
    4.14  \hspace*{0pt}\\
    4.15 -\hspace*{0pt}list{\char95}case ::~forall t a.~t -> (a -> [a] -> t) -> [a] -> t;\\
    4.16 +\hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\
    4.17  \hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
    4.18  \hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
    4.19  \hspace*{0pt}\\
     5.1 --- a/doc-src/Codegen/Thy/examples/Example.hs	Mon Aug 10 13:53:42 2009 +0200
     5.2 +++ b/doc-src/Codegen/Thy/examples/Example.hs	Tue Aug 11 20:40:02 2009 +0200
     5.3 @@ -3,14 +3,14 @@
     5.4  module Example where {
     5.5  
     5.6  
     5.7 -foldla :: forall a_1 b_1. (a_1 -> b_1 -> a_1) -> a_1 -> [b_1] -> a_1;
     5.8 +foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
     5.9  foldla f a [] = a;
    5.10  foldla f a (x : xs) = foldla f (f a x) xs;
    5.11  
    5.12  rev :: forall a. [a] -> [a];
    5.13  rev xs = foldla (\ xsa x -> x : xsa) [] xs;
    5.14  
    5.15 -list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;
    5.16 +list_case :: forall a b. a -> (b -> [b] -> a) -> [b] -> a;
    5.17  list_case f1 f2 (a : list) = f2 a list;
    5.18  list_case f1 f2 [] = f1;
    5.19  
     6.1 --- a/lib/Tools/version	Mon Aug 10 13:53:42 2009 +0200
     6.2 +++ b/lib/Tools/version	Tue Aug 11 20:40:02 2009 +0200
     6.3 @@ -4,5 +4,4 @@
     6.4  #
     6.5  # DESCRIPTION: display Isabelle version
     6.6  
     6.7 -
     6.8 -echo 'Isabelle repository version'    # filled in automatically!
     6.9 +echo 'unidentified repository version'    # filled in automatically!
     7.1 --- a/src/HOL/Code_Eval.thy	Mon Aug 10 13:53:42 2009 +0200
     7.2 +++ b/src/HOL/Code_Eval.thy	Tue Aug 11 20:40:02 2009 +0200
     7.3 @@ -39,6 +39,17 @@
     7.4  
     7.5  subsubsection {* @{text term_of} instances *}
     7.6  
     7.7 +instantiation "fun" :: (typerep, typerep) term_of
     7.8 +begin
     7.9 +
    7.10 +definition
    7.11 +  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
    7.12 +     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    7.13 +
    7.14 +instance ..
    7.15 +
    7.16 +end
    7.17 +
    7.18  setup {*
    7.19  let
    7.20    fun add_term_of tyco raw_vs thy =
     8.1 --- a/src/HOL/Fun.thy	Mon Aug 10 13:53:42 2009 +0200
     8.2 +++ b/src/HOL/Fun.thy	Tue Aug 11 20:40:02 2009 +0200
     8.3 @@ -250,6 +250,9 @@
     8.4  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
     8.5  by (simp add: bij_betw_def)
     8.6  
     8.7 +lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
     8.8 +by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
     8.9 +
    8.10  lemma bij_betw_trans:
    8.11    "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
    8.12  by(auto simp add:bij_betw_def comp_inj_on)
    10.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Aug 10 13:53:42 2009 +0200
    10.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Aug 11 20:40:02 2009 +0200
    10.3 @@ -167,7 +167,7 @@
    10.4      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    10.5    in
    10.6      if forall (can dest) thms andalso exists (contains_suc o dest) thms
    10.7 -      then perhaps_loop (remove_suc thy) thms
    10.8 +      then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
    10.9         else NONE
   10.10    end;
   10.11  
    11.1 --- a/src/HOL/Library/Nat_Int_Bij.thy	Mon Aug 10 13:53:42 2009 +0200
    11.2 +++ b/src/HOL/Library/Nat_Int_Bij.thy	Tue Aug 11 20:40:02 2009 +0200
    11.3 @@ -165,5 +165,11 @@
    11.4  lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
    11.5  by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
    11.6  
    11.7 +lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
    11.8 +by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
    11.9 +
   11.10 +lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
   11.11 +by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
   11.12 +
   11.13  
   11.14  end
    12.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Mon Aug 10 13:53:42 2009 +0200
    12.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Aug 11 20:40:02 2009 +0200
    12.3 @@ -1,12 +1,11 @@
    12.4  (*  Title:      HOL/MicroJava/J/JListExample.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Stefan Berghofer
    12.7  *)
    12.8  
    12.9  header {* \isaheader{Example for generating executable code from Java semantics} *}
   12.10  
   12.11  theory JListExample
   12.12 -imports Eval SystemClasses
   12.13 +imports Eval
   12.14  begin
   12.15  
   12.16  ML {* Syntax.ambiguity_level := 100000 *}
    13.1 --- a/src/HOL/MicroJava/J/State.thy	Mon Aug 10 13:53:42 2009 +0200
    13.2 +++ b/src/HOL/MicroJava/J/State.thy	Tue Aug 11 20:40:02 2009 +0200
    13.3 @@ -1,12 +1,13 @@
    13.4  (*  Title:      HOL/MicroJava/J/State.thy
    13.5 -    ID:         $Id$
    13.6      Author:     David von Oheimb
    13.7      Copyright   1999 Technische Universitaet Muenchen
    13.8  *)
    13.9  
   13.10  header {* \isaheader{Program State} *}
   13.11  
   13.12 -theory State imports TypeRel Value begin
   13.13 +theory State
   13.14 +imports TypeRel Value
   13.15 +begin
   13.16  
   13.17  types 
   13.18    fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
   13.19 @@ -19,7 +20,6 @@
   13.20  
   13.21    init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
   13.22   "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
   13.23 -  
   13.24  
   13.25  types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
   13.26        locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
    14.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Aug 10 13:53:42 2009 +0200
    14.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Aug 11 20:40:02 2009 +0200
    14.3 @@ -1,11 +1,12 @@
    14.4  (*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
    14.5 -    ID:         $Id$
    14.6      Author:     Stefan Berghofer
    14.7  *)
    14.8  
    14.9  header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
   14.10  
   14.11 -theory JVMListExample imports "../J/SystemClasses" JVMExec begin
   14.12 +theory JVMListExample
   14.13 +imports "../J/SystemClasses" JVMExec
   14.14 +begin
   14.15  
   14.16  consts
   14.17    list_nam :: cnam
    15.1 --- a/src/HOL/Tools/hologic.ML	Mon Aug 10 13:53:42 2009 +0200
    15.2 +++ b/src/HOL/Tools/hologic.ML	Tue Aug 11 20:40:02 2009 +0200
    15.3 @@ -67,14 +67,18 @@
    15.4    val split_const: typ * typ * typ -> term
    15.5    val mk_split: term -> term
    15.6    val flatten_tupleT: typ -> typ list
    15.7 -  val mk_tupleT: int list list -> typ list -> typ
    15.8 -  val strip_tupleT: int list list -> typ -> typ list
    15.9 +  val mk_tupleT: typ list -> typ
   15.10 +  val strip_tupleT: typ -> typ list
   15.11 +  val mk_tuple: term list -> term
   15.12 +  val strip_tuple: term -> term list
   15.13 +  val mk_ptupleT: int list list -> typ list -> typ
   15.14 +  val strip_ptupleT: int list list -> typ -> typ list
   15.15    val flat_tupleT_paths: typ -> int list list
   15.16 -  val mk_tuple: int list list -> typ -> term list -> term
   15.17 -  val dest_tuple: int list list -> term -> term list
   15.18 +  val mk_ptuple: int list list -> typ -> term list -> term
   15.19 +  val strip_ptuple: int list list -> term -> term list
   15.20    val flat_tuple_paths: term -> int list list
   15.21 -  val mk_splits: int list list -> typ -> typ -> term -> term
   15.22 -  val strip_splits: term -> term * typ list * int list list
   15.23 +  val mk_psplits: int list list -> typ -> typ -> term -> term
   15.24 +  val strip_psplits: term -> term * typ list * int list list
   15.25    val natT: typ
   15.26    val zero: term
   15.27    val is_zero: term -> bool
   15.28 @@ -118,6 +122,8 @@
   15.29    val mk_literal: string -> term
   15.30    val dest_literal: term -> string
   15.31    val mk_typerep: typ -> term
   15.32 +  val termT: typ
   15.33 +  val term_of_const: typ -> term
   15.34    val mk_term_of: typ -> term -> term
   15.35    val reflect_term: term -> term
   15.36    val mk_valtermify_app: string -> (string * typ) list -> typ -> term
   15.37 @@ -321,15 +327,33 @@
   15.38  fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
   15.39    | flatten_tupleT T = [T];
   15.40  
   15.41 +
   15.42 +(* tuples with right-fold structure *)
   15.43 +
   15.44 +fun mk_tupleT [] = unitT
   15.45 +  | mk_tupleT Ts = foldr1 mk_prodT Ts;
   15.46 +
   15.47 +fun strip_tupleT (Type ("Product_Type.unit", [])) = []
   15.48 +  | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
   15.49 +  | strip_tupleT T = [T];
   15.50 +
   15.51 +fun mk_tuple [] = unit
   15.52 +  | mk_tuple ts = foldr1 mk_prod ts;
   15.53 +
   15.54 +fun strip_tuple (Const ("Product_Type.Unity", _)) = []
   15.55 +  | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
   15.56 +  | strip_tuple t = [t];
   15.57 +
   15.58 +
   15.59  (* tuples with specific arities
   15.60  
   15.61 -  an "arity" of a tuple is a list of lists of integers
   15.62 -  ("factors"), denoting paths to subterms that are pairs
   15.63 +   an "arity" of a tuple is a list of lists of integers,
   15.64 +   denoting paths to subterms that are pairs
   15.65  *)
   15.66  
   15.67 -fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
   15.68 +fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
   15.69  
   15.70 -fun mk_tupleT ps =
   15.71 +fun mk_ptupleT ps =
   15.72    let
   15.73      fun mk p Ts =
   15.74        if p mem ps then
   15.75 @@ -340,12 +364,12 @@
   15.76        else (hd Ts, tl Ts)
   15.77    in fst o mk [] end;
   15.78  
   15.79 -fun strip_tupleT ps =
   15.80 +fun strip_ptupleT ps =
   15.81    let
   15.82      fun factors p T = if p mem ps then (case T of
   15.83          Type ("*", [T1, T2]) =>
   15.84            factors (1::p) T1 @ factors (2::p) T2
   15.85 -      | _ => prod_err "strip_tupleT") else [T]
   15.86 +      | _ => ptuple_err "strip_ptupleT") else [T]
   15.87    in factors [] end;
   15.88  
   15.89  val flat_tupleT_paths =
   15.90 @@ -355,7 +379,7 @@
   15.91        | factors p _ = []
   15.92    in factors [] end;
   15.93  
   15.94 -fun mk_tuple ps =
   15.95 +fun mk_ptuple ps =
   15.96    let
   15.97      fun mk p T ts =
   15.98        if p mem ps then (case T of
   15.99 @@ -364,16 +388,16 @@
  15.100                val (t, ts') = mk (1::p) T1 ts;
  15.101                val (u, ts'') = mk (2::p) T2 ts'
  15.102              in (pair_const T1 T2 $ t $ u, ts'') end
  15.103 -        | _ => prod_err "mk_tuple")
  15.104 +        | _ => ptuple_err "mk_ptuple")
  15.105        else (hd ts, tl ts)
  15.106    in fst oo mk [] end;
  15.107  
  15.108 -fun dest_tuple ps =
  15.109 +fun strip_ptuple ps =
  15.110    let
  15.111      fun dest p t = if p mem ps then (case t of
  15.112          Const ("Pair", _) $ t $ u =>
  15.113            dest (1::p) t @ dest (2::p) u
  15.114 -      | _ => prod_err "dest_tuple") else [t]
  15.115 +      | _ => ptuple_err "strip_ptuple") else [t]
  15.116    in dest [] end;
  15.117  
  15.118  val flat_tuple_paths =
  15.119 @@ -383,24 +407,24 @@
  15.120        | factors p _ = []
  15.121    in factors [] end;
  15.122  
  15.123 -(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
  15.124 +(*In mk_psplits ps S T u, term u expects separate arguments for the factors of S,
  15.125    with result type T.  The call creates a new term expecting one argument
  15.126    of type S.*)
  15.127 -fun mk_splits ps T T3 u =
  15.128 +fun mk_psplits ps T T3 u =
  15.129    let
  15.130      fun ap ((p, T) :: pTs) =
  15.131            if p mem ps then (case T of
  15.132                Type ("*", [T1, T2]) =>
  15.133                  split_const (T1, T2, map snd pTs ---> T3) $
  15.134                    ap ((1::p, T1) :: (2::p, T2) :: pTs)
  15.135 -            | _ => prod_err "mk_splits")
  15.136 +            | _ => ptuple_err "mk_psplits")
  15.137            else Abs ("x", T, ap pTs)
  15.138        | ap [] =
  15.139            let val k = length ps
  15.140            in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
  15.141    in ap [([], T)] end;
  15.142  
  15.143 -val strip_splits =
  15.144 +val strip_psplits =
  15.145    let
  15.146      fun strip [] qs Ts t = (t, Ts, qs)
  15.147        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
  15.148 @@ -591,7 +615,9 @@
  15.149  
  15.150  val termT = Type ("Code_Eval.term", []);
  15.151  
  15.152 -fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
  15.153 +fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
  15.154 +
  15.155 +fun mk_term_of T t = term_of_const T $ t;
  15.156  
  15.157  fun reflect_term (Const (c, T)) =
  15.158        Const ("Code_Eval.Const", literalT --> typerepT --> termT)
    16.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Aug 10 13:53:42 2009 +0200
    16.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Aug 11 20:40:02 2009 +0200
    16.3 @@ -645,7 +645,7 @@
    16.4  
    16.5  fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
    16.6      (Const ("Collect", _), [u]) =>
    16.7 -      let val (r, Ts, fs) = HOLogic.strip_splits u
    16.8 +      let val (r, Ts, fs) = HOLogic.strip_psplits u
    16.9        in case strip_comb r of
   16.10            (Const (s, T), ts) =>
   16.11              (case (get_clauses thy s, get_assoc_code thy (s, T)) of
    17.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Aug 10 13:53:42 2009 +0200
    17.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Aug 11 20:40:02 2009 +0200
    17.3 @@ -34,10 +34,10 @@
    17.4  val collect_mem_simproc =
    17.5    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
    17.6      fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
    17.7 -         let val (u, Ts, ps) = HOLogic.strip_splits t
    17.8 +         let val (u, Ts, ps) = HOLogic.strip_psplits t
    17.9           in case u of
   17.10             (c as Const ("op :", _)) $ q $ S' =>
   17.11 -             (case try (HOLogic.dest_tuple ps) q of
   17.12 +             (case try (HOLogic.strip_ptuple ps) q of
   17.13                  NONE => NONE
   17.14                | SOME ts =>
   17.15                    if not (loose_bvar (S', 0)) andalso
   17.16 @@ -80,7 +80,7 @@
   17.17        fun mk_collect p T t =
   17.18          let val U = HOLogic.dest_setT T
   17.19          in HOLogic.Collect_const U $
   17.20 -          HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
   17.21 +          HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
   17.22          end;
   17.23        fun decomp (Const (s, _) $ ((m as Const ("op :",
   17.24              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
   17.25 @@ -224,11 +224,11 @@
   17.26    map (fn (x, ps) =>
   17.27      let
   17.28        val U = HOLogic.dest_setT (fastype_of x);
   17.29 -      val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
   17.30 +      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
   17.31      in
   17.32        (cterm_of thy x,
   17.33         cterm_of thy (HOLogic.Collect_const U $
   17.34 -         HOLogic.mk_splits ps U HOLogic.boolT x'))
   17.35 +         HOLogic.mk_psplits ps U HOLogic.boolT x'))
   17.36      end) fs;
   17.37  
   17.38  fun mk_to_pred_eq p fs optfs' T thm =
   17.39 @@ -241,7 +241,7 @@
   17.40        | SOME fs' =>
   17.41            let
   17.42              val (_, U) = split_last (binder_types T);
   17.43 -            val Ts = HOLogic.strip_tupleT fs' U;
   17.44 +            val Ts = HOLogic.strip_ptupleT fs' U;
   17.45              (* FIXME: should cterm_instantiate increment indexes? *)
   17.46              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
   17.47              val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
   17.48 @@ -249,7 +249,7 @@
   17.49            in
   17.50              thm' RS (Drule.cterm_instantiate [(arg_cong_f,
   17.51                cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
   17.52 -                HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
   17.53 +                HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
   17.54                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
   17.55            end)
   17.56    in
   17.57 @@ -362,12 +362,12 @@
   17.58      val insts = map (fn (x, ps) =>
   17.59        let
   17.60          val Ts = binder_types (fastype_of x);
   17.61 -        val T = HOLogic.mk_tupleT ps Ts;
   17.62 +        val T = HOLogic.mk_ptupleT ps Ts;
   17.63          val x' = map_type (K (HOLogic.mk_setT T)) x
   17.64        in
   17.65          (cterm_of thy x,
   17.66           cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
   17.67 -           (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
   17.68 +           (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
   17.69        end) fs
   17.70    in
   17.71      thm |>
   17.72 @@ -423,14 +423,14 @@
   17.73          SOME fs =>
   17.74            let
   17.75              val T = HOLogic.dest_setT (fastype_of x);
   17.76 -            val Ts = HOLogic.strip_tupleT fs T;
   17.77 +            val Ts = HOLogic.strip_ptupleT fs T;
   17.78              val x' = map_type (K (Ts ---> HOLogic.boolT)) x
   17.79            in
   17.80              (x, (x',
   17.81                (HOLogic.Collect_const T $
   17.82 -                 HOLogic.mk_splits fs T HOLogic.boolT x',
   17.83 +                 HOLogic.mk_psplits fs T HOLogic.boolT x',
   17.84                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
   17.85 -                 (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
   17.86 +                 (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
   17.87                    x)))))
   17.88            end
   17.89         | NONE => (x, (x, (x, x))))) params;
   17.90 @@ -449,13 +449,13 @@
   17.91             Pretty.str ("of " ^ s ^ " do not agree with types"),
   17.92             Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
   17.93             Pretty.str "of declared parameters"]));
   17.94 -        val Ts = HOLogic.strip_tupleT fs U;
   17.95 +        val Ts = HOLogic.strip_ptupleT fs U;
   17.96          val c' = Free (s ^ "p",
   17.97            map fastype_of params1 @ Ts ---> HOLogic.boolT)
   17.98        in
   17.99          ((c', (fs, U, Ts)),
  17.100           (list_comb (c, params2),
  17.101 -          HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
  17.102 +          HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
  17.103              (list_comb (c', params1))))
  17.104        end) |> split_list |>> split_list;
  17.105      val eqns' = eqns @
  17.106 @@ -485,7 +485,7 @@
  17.107      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
  17.108        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
  17.109           fold_rev lambda params (HOLogic.Collect_const U $
  17.110 -           HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
  17.111 +           HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
  17.112           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
  17.113  
  17.114      (* prove theorems for converting predicate to set notation *)
  17.115 @@ -496,7 +496,7 @@
  17.116              (HOLogic.mk_Trueprop (HOLogic.mk_eq
  17.117                (list_comb (p, params3),
  17.118                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
  17.119 -                 (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
  17.120 +                 (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
  17.121                    list_comb (c, params))))))
  17.122              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
  17.123                [def, mem_Collect_eq, split_conv]) 1))
    18.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Mon Aug 10 13:53:42 2009 +0200
    18.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Aug 11 20:40:02 2009 +0200
    18.3 @@ -40,9 +40,10 @@
    18.4    let
    18.5      val fun_upd = Const (@{const_name fun_upd},
    18.6        (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    18.7 -    val (seed', seed'') = random_split seed;
    18.8 +    val ((y, t2), seed') = random seed;
    18.9 +    val (seed'', seed''') = random_split seed';
   18.10  
   18.11 -    val state = ref (seed', [], fn () => Const (@{const_name undefined}, T1 --> T2));
   18.12 +    val state = ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
   18.13      fun random_fun' x =
   18.14        let
   18.15          val (seed, fun_map, f_t) = ! state;
   18.16 @@ -57,7 +58,7 @@
   18.17              in y end
   18.18        end;
   18.19      fun term_fun' () = #3 (! state) ();
   18.20 -  in ((random_fun', term_fun'), seed'') end;
   18.21 +  in ((random_fun', term_fun'), seed''') end;
   18.22  
   18.23  
   18.24  (** type copies **)
    19.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon Aug 10 13:53:42 2009 +0200
    19.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Aug 11 20:40:02 2009 +0200
    19.3 @@ -14,6 +14,8 @@
    19.4  
    19.5  open Codegen;
    19.6  
    19.7 +val const_of = dest_Const o head_of o fst o Logic.dest_equals;
    19.8 +
    19.9  structure ModuleData = TheoryDataFun
   19.10  (
   19.11    type T = string Symtab.table;
   19.12 @@ -31,43 +33,32 @@
   19.13      |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
   19.14    end;
   19.15  
   19.16 -fun expand_eta thy [] = []
   19.17 -  | expand_eta thy (thms as thm :: _) =
   19.18 -      let
   19.19 -        val (_, ty) = Code.const_typ_eqn thy thm;
   19.20 -      in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
   19.21 -        then thms
   19.22 -        else map (Code.expand_eta thy 1) thms
   19.23 -      end;
   19.24 +fun avoid_value thy [thm] =
   19.25 +      let val (_, T) = Code.const_typ_eqn thy thm
   19.26 +      in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
   19.27 +        then [thm]
   19.28 +        else [Code_Thingol.expand_eta thy 1 thm]
   19.29 +      end
   19.30 +  | avoid_value thy thms = thms;
   19.31  
   19.32 -fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
   19.33 +fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
   19.34    let
   19.35 -    val c' = AxClass.unoverload_const thy (c, T);
   19.36 -    val opt_name = Symtab.lookup (ModuleData.get thy) c';
   19.37 -    val thms = Code.these_eqns thy c'
   19.38 +    val c = AxClass.unoverload_const thy (raw_c, T);
   19.39 +    val raw_thms = Code.these_eqns thy c
   19.40        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
   19.41 -      |> expand_eta thy
   19.42 -      |> Code.norm_varnames thy
   19.43 -      |> map (rpair opt_name)
   19.44 -  in if null thms then NONE else SOME thms end;
   19.45 -
   19.46 -val dest_eqn = Logic.dest_equals;
   19.47 -val const_of = dest_Const o head_of o fst o dest_eqn;
   19.48 -
   19.49 -fun get_equations thy defs (s, T) =
   19.50 -  (case retrieve_equations thy (s, T) of
   19.51 -     NONE => ([], "")
   19.52 -   | SOME thms => 
   19.53 -       let val thms' = filter (fn (thm, _) => is_instance T
   19.54 -           (snd (const_of (prop_of thm)))) thms
   19.55 -       in if null thms' then ([], "")
   19.56 -         else (preprocess thy (map fst thms'),
   19.57 -           case snd (snd (split_last thms')) of
   19.58 -               NONE => (case get_defn thy defs s T of
   19.59 -                   NONE => Codegen.thyname_of_const thy s
   19.60 -                 | SOME ((_, (thyname, _)), _) => thyname)
   19.61 -             | SOME thyname => thyname)
   19.62 -       end);
   19.63 +      |> filter (is_instance T o snd o const_of o prop_of);
   19.64 +    val module_name = case Symtab.lookup (ModuleData.get thy) c
   19.65 +     of SOME module_name => module_name
   19.66 +      | NONE => case get_defn thy defs c T
   19.67 +         of SOME ((_, (thyname, _)), _) => thyname
   19.68 +          | NONE => Codegen.thyname_of_const thy c;
   19.69 +  in if null raw_thms then ([], "") else
   19.70 +    raw_thms
   19.71 +    |> preprocess thy
   19.72 +    |> avoid_value thy
   19.73 +    |> Code_Thingol.clean_thms thy
   19.74 +    |> rpair module_name
   19.75 +  end;
   19.76  
   19.77  fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
   19.78    SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
   19.79 @@ -81,7 +72,7 @@
   19.80  fun add_rec_funs thy defs dep module eqs gr =
   19.81    let
   19.82      fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
   19.83 -      dest_eqn (rename_term t));
   19.84 +      Logic.dest_equals (rename_term t));
   19.85      val eqs' = map dest_eq eqs;
   19.86      val (dname, _) :: _ = eqs';
   19.87      val (s, T) = const_of (hd eqs);
    20.1 --- a/src/HOL/Tools/split_rule.ML	Mon Aug 10 13:53:42 2009 +0200
    20.2 +++ b/src/HOL/Tools/split_rule.ML	Tue Aug 11 20:40:02 2009 +0200
    20.3 @@ -81,7 +81,7 @@
    20.4                let
    20.5                  val Ts = HOLogic.flatten_tupleT T;
    20.6                  val ys = Name.variant_list xs (replicate (length Ts) a);
    20.7 -              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T
    20.8 +              in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
    20.9                  (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
   20.10                end
   20.11            | mk_tuple _ x = x;
    21.1 --- a/src/HOL/ex/Predicate_Compile.thy	Mon Aug 10 13:53:42 2009 +0200
    21.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Tue Aug 11 20:40:02 2009 +0200
    21.3 @@ -1,61 +1,8 @@
    21.4  theory Predicate_Compile
    21.5 -imports Main Lattice_Syntax Code_Eval RPred
    21.6 +imports Complex_Main RPred
    21.7  uses "predicate_compile.ML"
    21.8  begin
    21.9  
   21.10 -text {* Package setup *}
   21.11 -
   21.12  setup {* Predicate_Compile.setup *}
   21.13  
   21.14 -text {* Experimental code *}
   21.15 -
   21.16 -ML {*
   21.17 -structure Predicate_Compile =
   21.18 -struct
   21.19 -
   21.20 -open Predicate_Compile;
   21.21 -
   21.22 -fun eval thy t_compr =
   21.23 -  let
   21.24 -    val t = Predicate_Compile.analyze_compr thy t_compr;
   21.25 -    val Type (@{type_name Predicate.pred}, [T]) = fastype_of t;
   21.26 -    fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
   21.27 -    val T1 = T --> @{typ term};
   21.28 -    val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
   21.29 -    val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
   21.30 -      $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
   21.31 -  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
   21.32 -
   21.33 -fun values ctxt k t_compr =
   21.34 -  let
   21.35 -    val thy = ProofContext.theory_of ctxt;
   21.36 -    val (T, t') = eval thy t_compr;
   21.37 -  in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end;
   21.38 -
   21.39 -fun values_cmd modes k raw_t state =
   21.40 -  let
   21.41 -    val ctxt = Toplevel.context_of state;
   21.42 -    val t = Syntax.read_term ctxt raw_t;
   21.43 -    val t' = values ctxt k t;
   21.44 -    val ty' = Term.type_of t';
   21.45 -    val ctxt' = Variable.auto_fixes t' ctxt;
   21.46 -    val p = PrintMode.with_modes modes (fn () =>
   21.47 -      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   21.48 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   21.49 -  in Pretty.writeln p end;
   21.50 -
   21.51 -end;
   21.52 -
   21.53 -local structure P = OuterParse in
   21.54 -
   21.55 -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   21.56 -
   21.57 -val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
   21.58 -  (opt_modes -- Scan.optional P.nat ~1 -- P.term
   21.59 -    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
   21.60 -        (Predicate_Compile.values_cmd modes k t)));
   21.61 -
   21.62 -end;
   21.63 -*}
   21.64 -
   21.65  end
   21.66 \ No newline at end of file
    22.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Mon Aug 10 13:53:42 2009 +0200
    22.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Aug 11 20:40:02 2009 +0200
    22.3 @@ -18,15 +18,10 @@
    22.4  values 10 "{n. odd n}"
    22.5  
    22.6  inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    22.7 -    append_Nil: "append [] xs xs"
    22.8 -  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    22.9 +    "append [] xs xs"
   22.10 +  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
   22.11  
   22.12 -inductive rev
   22.13 -where
   22.14 -"rev [] []"
   22.15 -| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   22.16 -
   22.17 -code_pred rev .
   22.18 +code_pred append .
   22.19  
   22.20  thm append.equation
   22.21  
   22.22 @@ -34,6 +29,15 @@
   22.23  values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
   22.24  values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}"
   22.25  
   22.26 +inductive rev where
   22.27 +    "rev [] []"
   22.28 +  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   22.29 +
   22.30 +code_pred rev .
   22.31 +
   22.32 +thm rev.equation
   22.33 +
   22.34 +values "{xs. rev [0, 1, 2, 3::nat] xs}"
   22.35  
   22.36  inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   22.37    for f where
   22.38 @@ -51,17 +55,15 @@
   22.39  
   22.40  code_pred is_even .
   22.41  
   22.42 -(* TODO: requires to handle abstractions in parameter positions correctly *)
   22.43  values 10 "{(ys, zs). partition is_even
   22.44    [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
   22.45 -
   22.46  values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
   22.47  values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
   22.48  
   22.49  lemma [code_pred_intros]:
   22.50 -"r a b ==> tranclp r a b"
   22.51 -"r a b ==> tranclp r b c ==> tranclp r a c"
   22.52 -by auto
   22.53 +  "r a b \<Longrightarrow> tranclp r a b"
   22.54 +  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   22.55 +  by auto
   22.56  
   22.57  code_pred tranclp
   22.58  proof -
   22.59 @@ -76,6 +78,7 @@
   22.60  
   22.61  thm tranclp.rpred_equation
   22.62  *)
   22.63 +
   22.64  inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   22.65      "succ 0 1"
   22.66    | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
   22.67 @@ -83,7 +86,13 @@
   22.68  code_pred succ .
   22.69  
   22.70  thm succ.equation
   22.71 +
   22.72 +values 10 "{(m, n). succ n m}"
   22.73 +values "{m. succ 0 m}"
   22.74 +values "{m. succ m 0}"
   22.75 +
   22.76  (* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *)
   22.77 +
   22.78  (*
   22.79  values 20 "{n. tranclp succ 10 n}"
   22.80  values "{n. tranclp succ n 10}"
    23.1 --- a/src/HOL/ex/predicate_compile.ML	Mon Aug 10 13:53:42 2009 +0200
    23.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Aug 11 20:40:02 2009 +0200
    23.3 @@ -54,6 +54,7 @@
    23.4      mk_sup : term * term -> term,
    23.5      mk_if : term -> term,
    23.6      mk_not : term -> term,
    23.7 +    mk_map : typ -> typ -> term -> term -> term,
    23.8      lift_pred : term -> term
    23.9    };  
   23.10    datatype tmode = Mode of mode * int list * tmode option list;
   23.11 @@ -608,6 +609,7 @@
   23.12    mk_not : term -> term,
   23.13  (*  funT_of : mode -> typ -> typ, *)
   23.14  (*  mk_fun_of : theory -> (string * typ) -> mode -> term, *) 
   23.15 +  mk_map : typ -> typ -> term -> term -> term,
   23.16    lift_pred : term -> term
   23.17  };
   23.18  
   23.19 @@ -621,6 +623,7 @@
   23.20  fun mk_not (CompilationFuns funs) = #mk_not funs
   23.21  (*fun funT_of (CompilationFuns funs) = #funT_of funs*)
   23.22  (*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*)
   23.23 +fun mk_map (CompilationFuns funs) = #mk_map funs
   23.24  fun lift_pred (CompilationFuns funs) = #lift_pred funs
   23.25  
   23.26  fun funT_of compfuns (iss, is) T =
   23.27 @@ -691,12 +694,15 @@
   23.28    in
   23.29      Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
   23.30    end;
   23.31 -  
   23.32 +
   23.33 +fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
   23.34 +  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
   23.35 +
   23.36  val lift_pred = I
   23.37  
   23.38  val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   23.39    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
   23.40 -  lift_pred = lift_pred} 
   23.41 +  mk_map = mk_map, lift_pred = lift_pred};
   23.42  
   23.43  end;
   23.44  
   23.45 @@ -748,7 +754,9 @@
   23.46    HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
   23.47  
   23.48  fun mk_not t = error "Negation is not defined for RPred"
   23.49 -   
   23.50 +
   23.51 +fun mk_map t = error "FIXME" (*FIXME*)
   23.52 +
   23.53  fun lift_pred t =
   23.54    let
   23.55      val T = PredicateCompFuns.dest_predT (fastype_of t)
   23.56 @@ -759,7 +767,7 @@
   23.57  
   23.58  val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
   23.59      mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
   23.60 -    lift_pred = lift_pred} 
   23.61 +    mk_map = mk_map, lift_pred = lift_pred};
   23.62  
   23.63  end;
   23.64  (* for external use with interactive mode *)
   23.65 @@ -2094,18 +2102,17 @@
   23.66  
   23.67  val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
   23.68  
   23.69 +(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
   23.70  fun analyze_compr thy t_compr =
   23.71    let
   23.72      val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
   23.73        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
   23.74 -    val (body, Ts, fp) = HOLogic.strip_splits split;
   23.75 -      (*FIXME former order of tuple positions must be restored*)
   23.76 -    val (pred as Const (name, T), all_args) = strip_comb body
   23.77 -    val (params, args) = chop (nparams_of thy name) all_args
   23.78 +    val (body, Ts, fp) = HOLogic.strip_psplits split;
   23.79 +    val (pred as Const (name, T), all_args) = strip_comb body;
   23.80 +    val (params, args) = chop (nparams_of thy name) all_args;
   23.81      val user_mode = map_filter I (map_index
   23.82        (fn (i, t) => case t of Bound j => if j < length Ts then NONE
   23.83 -        else SOME (i+1) | _ => SOME (i+1)) args) (*FIXME dangling bounds should not occur*)
   23.84 -    val (inargs, _) = split_smode user_mode args;
   23.85 +        else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
   23.86      val modes = filter (fn Mode (_, is, _) => is = user_mode)
   23.87        (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
   23.88      val m = case modes
   23.89 @@ -2114,10 +2121,62 @@
   23.90        | [m] => m
   23.91        | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
   23.92                  ^ Syntax.string_of_term_global thy t_compr); m);
   23.93 -    val t_eval = list_comb (compile_expr NONE thy 
   23.94 -      (m, list_comb (pred, params)),
   23.95 -      inargs)
   23.96 +    val (inargs, outargs) = split_smode user_mode args;
   23.97 +    val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
   23.98 +    val t_eval = if null outargs then t_pred else let
   23.99 +        val outargs_bounds = map (fn Bound i => i) outargs;
  23.100 +        val outargsTs = map (nth Ts) outargs_bounds;
  23.101 +        val T_pred = HOLogic.mk_tupleT outargsTs;
  23.102 +        val T_compr = HOLogic.mk_ptupleT fp Ts;
  23.103 +        val arrange_bounds = map_index I outargs_bounds
  23.104 +          |> sort (prod_ord (K EQUAL) int_ord)
  23.105 +          |> map fst;
  23.106 +        val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
  23.107 +          (Term.list_abs (map (pair "") outargsTs,
  23.108 +            HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
  23.109 +      in mk_map PredicateCompFuns.compfuns T_pred T_compr arrange t_pred end
  23.110    in t_eval end;
  23.111  
  23.112 +fun eval thy t_compr =
  23.113 +  let
  23.114 +    val t = analyze_compr thy t_compr;
  23.115 +    val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
  23.116 +    val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
  23.117 +  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
  23.118 +
  23.119 +fun values ctxt k t_compr =
  23.120 +  let
  23.121 +    val thy = ProofContext.theory_of ctxt;
  23.122 +    val (T, t) = eval thy t_compr;
  23.123 +    val setT = HOLogic.mk_setT T;
  23.124 +    val (ts, _) = Predicate.yieldn k t;
  23.125 +    val elemsT = HOLogic.mk_set T ts;
  23.126 +  in if k = ~1 orelse length ts < k then elemsT
  23.127 +    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
  23.128 +  end;
  23.129 +
  23.130 +fun values_cmd modes k raw_t state =
  23.131 +  let
  23.132 +    val ctxt = Toplevel.context_of state;
  23.133 +    val t = Syntax.read_term ctxt raw_t;
  23.134 +    val t' = values ctxt k t;
  23.135 +    val ty' = Term.type_of t';
  23.136 +    val ctxt' = Variable.auto_fixes t' ctxt;
  23.137 +    val p = PrintMode.with_modes modes (fn () =>
  23.138 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
  23.139 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
  23.140 +  in Pretty.writeln p end;
  23.141 +
  23.142 +local structure P = OuterParse in
  23.143 +
  23.144 +val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
  23.145 +
  23.146 +val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
  23.147 +  (opt_modes -- Scan.optional P.nat ~1 -- P.term
  23.148 +    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
  23.149 +        (values_cmd modes k t)));
  23.150 +
  23.151  end;
  23.152  
  23.153 +end;
  23.154 +
    24.1 --- a/src/Pure/Isar/code.ML	Mon Aug 10 13:53:42 2009 +0200
    24.2 +++ b/src/Pure/Isar/code.ML	Tue Aug 11 20:40:02 2009 +0200
    24.3 @@ -33,9 +33,6 @@
    24.4      -> (thm * bool) list -> (thm * bool) list
    24.5    val const_typ_eqn: theory -> thm -> string * typ
    24.6    val typscheme_eqn: theory -> thm -> (string * sort) list * typ
    24.7 -  val expand_eta: theory -> int -> thm -> thm
    24.8 -  val norm_args: theory -> thm list -> thm list 
    24.9 -  val norm_varnames: theory -> thm list -> thm list
   24.10  
   24.11    (*executable code*)
   24.12    val add_datatype: (string * typ) list -> theory -> theory
   24.13 @@ -126,115 +123,6 @@
   24.14    in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
   24.15  
   24.16  
   24.17 -(* code equation transformations *)
   24.18 -
   24.19 -fun expand_eta thy k thm =
   24.20 -  let
   24.21 -    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
   24.22 -    val (head, args) = strip_comb lhs;
   24.23 -    val l = if k = ~1
   24.24 -      then (length o fst o strip_abs) rhs
   24.25 -      else Int.max (0, k - length args);
   24.26 -    val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
   24.27 -    fun get_name _ 0 = pair []
   24.28 -      | get_name (Abs (v, ty, t)) k =
   24.29 -          Name.variants [v]
   24.30 -          ##>> get_name t (k - 1)
   24.31 -          #>> (fn ([v'], vs') => (v', ty) :: vs')
   24.32 -      | get_name t k = 
   24.33 -          let
   24.34 -            val (tys, _) = (strip_type o fastype_of) t
   24.35 -          in case tys
   24.36 -           of [] => raise TERM ("expand_eta", [t])
   24.37 -            | ty :: _ =>
   24.38 -                Name.variants [""]
   24.39 -                #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
   24.40 -                #>> (fn vs' => (v, ty) :: vs'))
   24.41 -          end;
   24.42 -    val (vs, _) = get_name rhs l used;
   24.43 -    fun expand (v, ty) thm = Drule.fun_cong_rule thm
   24.44 -      (Thm.cterm_of thy (Var ((v, 0), ty)));
   24.45 -  in
   24.46 -    thm
   24.47 -    |> fold expand vs
   24.48 -    |> Conv.fconv_rule Drule.beta_eta_conversion
   24.49 -  end;
   24.50 -
   24.51 -fun norm_args thy thms =
   24.52 -  let
   24.53 -    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
   24.54 -    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
   24.55 -  in
   24.56 -    thms
   24.57 -    |> map (expand_eta thy k)
   24.58 -    |> map (Conv.fconv_rule Drule.beta_eta_conversion)
   24.59 -  end;
   24.60 -
   24.61 -fun canonical_tvars thy thm =
   24.62 -  let
   24.63 -    val ctyp = Thm.ctyp_of thy;
   24.64 -    val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
   24.65 -    fun tvars_subst_for thm = (fold_types o fold_atyps)
   24.66 -      (fn TVar (v_i as (v, _), sort) => let
   24.67 -            val v' = purify_tvar v
   24.68 -          in if v = v' then I
   24.69 -          else insert (op =) (v_i, (v', sort)) end
   24.70 -        | _ => I) (prop_of thm) [];
   24.71 -    fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
   24.72 -      let
   24.73 -        val ty = TVar (v_i, sort)
   24.74 -      in
   24.75 -        (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
   24.76 -      end;
   24.77 -    val maxidx = Thm.maxidx_of thm + 1;
   24.78 -    val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
   24.79 -  in Thm.instantiate (inst, []) thm end;
   24.80 -
   24.81 -fun canonical_vars thy thm =
   24.82 -  let
   24.83 -    val cterm = Thm.cterm_of thy;
   24.84 -    val purify_var = Name.desymbolize false;
   24.85 -    fun vars_subst_for thm = fold_aterms
   24.86 -      (fn Var (v_i as (v, _), ty) => let
   24.87 -            val v' = purify_var v
   24.88 -          in if v = v' then I
   24.89 -          else insert (op =) (v_i, (v', ty)) end
   24.90 -        | _ => I) (prop_of thm) [];
   24.91 -    fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
   24.92 -      let
   24.93 -        val t = Var (v_i, ty)
   24.94 -      in
   24.95 -        (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
   24.96 -      end;
   24.97 -    val maxidx = Thm.maxidx_of thm + 1;
   24.98 -    val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
   24.99 -  in Thm.instantiate ([], inst) thm end;
  24.100 -
  24.101 -fun canonical_absvars thm =
  24.102 -  let
  24.103 -    val t = Thm.plain_prop_of thm;
  24.104 -    val purify_var = Name.desymbolize false;
  24.105 -    val t' = Term.map_abs_vars purify_var t;
  24.106 -  in Thm.rename_boundvars t t' thm end;
  24.107 -
  24.108 -fun norm_varnames thy thms =
  24.109 -  let
  24.110 -    fun burrow_thms f [] = []
  24.111 -      | burrow_thms f thms =
  24.112 -          thms
  24.113 -          |> Conjunction.intr_balanced
  24.114 -          |> f
  24.115 -          |> Conjunction.elim_balanced (length thms)
  24.116 -  in
  24.117 -    thms
  24.118 -    |> map (canonical_vars thy)
  24.119 -    |> map canonical_absvars
  24.120 -    |> map Drule.zero_var_indexes
  24.121 -    |> burrow_thms (canonical_tvars thy)
  24.122 -    |> Drule.zero_var_indexes_list
  24.123 -  end;
  24.124 -
  24.125 -
  24.126  (** data store **)
  24.127  
  24.128  (* code equations *)
  24.129 @@ -662,32 +550,21 @@
  24.130          ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
  24.131    in map (cert o assert_eqn thy) eqns end;
  24.132  
  24.133 -fun common_typ_eqns thy [] = []
  24.134 -  | common_typ_eqns thy [thm] = [thm]
  24.135 -  | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*)
  24.136 -      let
  24.137 -        fun incr_thm thm max =
  24.138 -          let
  24.139 -            val thm' = incr_indexes max thm;
  24.140 -            val max' = Thm.maxidx_of thm' + 1;
  24.141 -          in (thm', max') end;
  24.142 -        val (thms', maxidx) = fold_map incr_thm thms 0;
  24.143 -        val ty1 :: tys = map (snd o const_typ_eqn thy) thms';
  24.144 -        fun unify ty env = Sign.typ_unify thy (ty1, ty) env
  24.145 -          handle Type.TUNIFY =>
  24.146 -            error ("Type unificaton failed, while unifying code equations\n"
  24.147 -            ^ (cat_lines o map (Display.string_of_thm_global thy)) thms
  24.148 -            ^ "\nwith types\n"
  24.149 -            ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
  24.150 -        val (env, _) = fold unify tys (Vartab.empty, maxidx)
  24.151 -        val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
  24.152 -          cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
  24.153 -      in map (Thm.instantiate (instT, [])) thms' end;
  24.154 +fun same_typscheme thy thms =
  24.155 +  let
  24.156 +    fun tvars_of t = rev (Term.add_tvars t []);
  24.157 +    val vss = map (tvars_of o Thm.prop_of) thms;
  24.158 +    fun inter_sorts vs =
  24.159 +      fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
  24.160 +    val sorts = map_transpose inter_sorts vss;
  24.161 +    val vts = Name.names Name.context Name.aT sorts
  24.162 +      |> map (fn (v, sort) => TVar ((v, 0), sort));
  24.163 +  in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
  24.164  
  24.165  fun these_eqns thy c =
  24.166    get_eqns thy c
  24.167    |> (map o apfst) (Thm.transfer thy)
  24.168 -  |> burrow_fst (common_typ_eqns thy);
  24.169 +  |> burrow_fst (same_typscheme thy);
  24.170  
  24.171  fun all_eqns thy =
  24.172    Symtab.dest ((the_eqns o the_exec) thy)
    25.1 --- a/src/Pure/Isar/overloading.ML	Mon Aug 10 13:53:42 2009 +0200
    25.2 +++ b/src/Pure/Isar/overloading.ML	Tue Aug 11 20:40:02 2009 +0200
    25.3 @@ -132,36 +132,42 @@
    25.4    |> get_first (fn ((c, _), (v, checked)) =>
    25.5        if Binding.name_of b = v then SOME (c, checked) else NONE);
    25.6  
    25.7 -fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));
    25.8 +
    25.9 +(* target *)
   25.10  
   25.11 +fun synchronize_syntax ctxt =
   25.12 +  let
   25.13 +    val overloading = OverloadingData.get ctxt;
   25.14 +    fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
   25.15 +     of SOME (v, _) => SOME (ty, Free (v, ty))
   25.16 +      | NONE => NONE;
   25.17 +    val unchecks =
   25.18 +      map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
   25.19 +  in 
   25.20 +    ctxt
   25.21 +    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
   25.22 +  end
   25.23  
   25.24 -(* overloaded declarations and definitions *)
   25.25 +fun init raw_overloading thy =
   25.26 +  let
   25.27 +    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
   25.28 +    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
   25.29 +  in
   25.30 +    thy
   25.31 +    |> ProofContext.init
   25.32 +    |> OverloadingData.put overloading
   25.33 +    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
   25.34 +    |> add_improvable_syntax
   25.35 +    |> synchronize_syntax
   25.36 +  end;
   25.37  
   25.38  fun declare c_ty = pair (Const c_ty);
   25.39  
   25.40  fun define checked b (c, t) = Thm.add_def (not checked) true
   25.41    (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
   25.42  
   25.43 -
   25.44 -(* target *)
   25.45 -
   25.46 -fun init raw_overloading thy =
   25.47 -  let
   25.48 -    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
   25.49 -    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
   25.50 -    fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
   25.51 -     of SOME (v, _) => SOME (ty, Free (v, ty))
   25.52 -      | NONE => NONE;
   25.53 -    val unchecks =
   25.54 -      map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
   25.55 -  in
   25.56 -    thy
   25.57 -    |> ProofContext.init
   25.58 -    |> OverloadingData.put overloading
   25.59 -    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
   25.60 -    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
   25.61 -    |> add_improvable_syntax
   25.62 -  end;
   25.63 +fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
   25.64 +  #> LocalTheory.target synchronize_syntax
   25.65  
   25.66  fun conclude lthy =
   25.67    let
    26.1 --- a/src/Pure/ROOT.ML	Mon Aug 10 13:53:42 2009 +0200
    26.2 +++ b/src/Pure/ROOT.ML	Tue Aug 11 20:40:02 2009 +0200
    26.3 @@ -2,7 +2,7 @@
    26.4  
    26.5  structure Distribution =     (*filled-in by makedist*)
    26.6  struct
    26.7 -  val version = "Isabelle repository version";
    26.8 +  val version = "unidentified repository version";
    26.9    val is_official = false;
   26.10    val changelog = "";
   26.11  end;
    27.1 --- a/src/Pure/library.ML	Mon Aug 10 13:53:42 2009 +0200
    27.2 +++ b/src/Pure/library.ML	Tue Aug 11 20:40:02 2009 +0200
    27.3 @@ -109,6 +109,7 @@
    27.4    val split_list: ('a * 'b) list -> 'a list * 'b list
    27.5    val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    27.6    val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    27.7 +  val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
    27.8    val separate: 'a -> 'a list -> 'a list
    27.9    val surround: 'a -> 'a list -> 'a list
   27.10    val replicate: int -> 'a -> 'a list
   27.11 @@ -929,6 +930,17 @@
   27.12    in dups end;
   27.13  
   27.14  
   27.15 +(* matrices *)
   27.16 +
   27.17 +fun map_transpose f xss =
   27.18 +  let
   27.19 +    val n = case distinct (op =) (map length xss)
   27.20 +     of [] => 0
   27.21 +      | [n] => n
   27.22 +      | _ => raise UnequalLengths;
   27.23 +  in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
   27.24 +
   27.25 +
   27.26  
   27.27  (** lists as multisets **)
   27.28  
    28.1 --- a/src/Tools/Code/code_preproc.ML	Mon Aug 10 13:53:42 2009 +0200
    28.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Aug 11 20:40:02 2009 +0200
    28.3 @@ -109,7 +109,10 @@
    28.4    | apply_functrans thy c [] eqns = eqns
    28.5    | apply_functrans thy c functrans eqns = eqns
    28.6        |> perhaps (perhaps_loop (perhaps_apply functrans))
    28.7 -      |> Code.assert_eqns_const thy c;
    28.8 +      |> Code.assert_eqns_const thy c
    28.9 +      (*FIXME in future, the check here should be more accurate wrt. type schemes
   28.10 +      -- perhaps by means of upcoming code certificates with a corresponding
   28.11 +         preprocessor protocol*);
   28.12  
   28.13  fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   28.14  
   28.15 @@ -140,8 +143,6 @@
   28.16      |> (map o apfst) (rewrite_eqn pre)
   28.17      |> (map o apfst) (AxClass.unoverload thy)
   28.18      |> map (Code.assert_eqn thy)
   28.19 -    |> burrow_fst (Code.norm_args thy)
   28.20 -    |> burrow_fst (Code.norm_varnames thy)
   28.21    end;
   28.22  
   28.23  fun preprocess_conv thy ct =
    29.1 --- a/src/Tools/Code/code_thingol.ML	Mon Aug 10 13:53:42 2009 +0200
    29.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Aug 11 20:40:02 2009 +0200
    29.3 @@ -79,6 +79,8 @@
    29.4    val is_cons: program -> string -> bool
    29.5    val contr_classparam_typs: program -> string -> itype option list
    29.6  
    29.7 +  val expand_eta: theory -> int -> thm -> thm
    29.8 +  val clean_thms: theory -> thm list -> thm list
    29.9    val read_const_exprs: theory -> string list -> string list * string list
   29.10    val consts_program: theory -> string list -> string list * (naming * program)
   29.11    val cached_program: theory -> naming * program
   29.12 @@ -376,6 +378,60 @@
   29.13  end; (* local *)
   29.14  
   29.15  
   29.16 +(** technical transformations of code equations **)
   29.17 +
   29.18 +fun expand_eta thy k thm =
   29.19 +  let
   29.20 +    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
   29.21 +    val (head, args) = strip_comb lhs;
   29.22 +    val l = if k = ~1
   29.23 +      then (length o fst o strip_abs) rhs
   29.24 +      else Int.max (0, k - length args);
   29.25 +    val (raw_vars, _) = Term.strip_abs_eta l rhs;
   29.26 +    val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
   29.27 +      raw_vars;
   29.28 +    fun expand (v, ty) thm = Drule.fun_cong_rule thm
   29.29 +      (Thm.cterm_of thy (Var ((v, 0), ty)));
   29.30 +  in
   29.31 +    thm
   29.32 +    |> fold expand vars
   29.33 +    |> Conv.fconv_rule Drule.beta_eta_conversion
   29.34 +  end;
   29.35 +
   29.36 +fun same_arity thy thms =
   29.37 +  let
   29.38 +    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
   29.39 +    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
   29.40 +  in map (expand_eta thy k) thms end;
   29.41 +
   29.42 +fun mk_desymbolization pre post mk vs =
   29.43 +  let
   29.44 +    val names = map (pre o fst o fst) vs
   29.45 +      |> map (Name.desymbolize false)
   29.46 +      |> Name.variant_list []
   29.47 +      |> map post;
   29.48 +  in map_filter (fn (((v, i), x), v') =>
   29.49 +    if v = v' andalso i = 0 then NONE
   29.50 +    else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
   29.51 +  end;
   29.52 +
   29.53 +fun desymbolize_tvars thy thms =
   29.54 +  let
   29.55 +    val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
   29.56 +    val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
   29.57 +  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
   29.58 +
   29.59 +fun desymbolize_vars thy thm =
   29.60 +  let
   29.61 +    val vs = Term.add_vars (Thm.prop_of thm) [];
   29.62 +    val var_subst = mk_desymbolization I I Var vs;
   29.63 +  in Thm.certify_instantiate ([], var_subst) thm end;
   29.64 +
   29.65 +fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
   29.66 +
   29.67 +fun clean_thms thy = same_arity thy #> desymbolize_all_vars thy;
   29.68 +
   29.69 +
   29.70  (** statements, abstract programs **)
   29.71  
   29.72  type typscheme = (vname * sort) list * itype;
   29.73 @@ -498,17 +554,11 @@
   29.74      fun stmt_classparam class =
   29.75        ensure_class thy algbr funcgr class
   29.76        #>> (fn class => Classparam (c, class));
   29.77 -    fun stmt_fun ((vs, ty), raw_thms) =
   29.78 -      let
   29.79 -        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
   29.80 -          then raw_thms
   29.81 -          else (map o apfst) (Code.expand_eta thy 1) raw_thms;
   29.82 -      in
   29.83 -        fold_map (translate_tyvar_sort thy algbr funcgr) vs
   29.84 -        ##>> translate_typ thy algbr funcgr ty
   29.85 -        ##>> fold_map (translate_eq thy algbr funcgr) thms
   29.86 -        #>> (fn info => Fun (c, info))
   29.87 -      end;
   29.88 +    fun stmt_fun ((vs, ty), eqns) =
   29.89 +      fold_map (translate_tyvar_sort thy algbr funcgr) vs
   29.90 +      ##>> translate_typ thy algbr funcgr ty
   29.91 +      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns)
   29.92 +      #>> (fn info => Fun (c, info));
   29.93      val stmt_const = case Code.get_datatype_of_constr thy c
   29.94       of SOME tyco => stmt_datatypecons tyco
   29.95        | NONE => (case AxClass.class_of_param thy c
   29.96 @@ -597,7 +647,7 @@
   29.97              translate_term thy algbr funcgr thm t'
   29.98              ##>> fold_map (translate_term thy algbr funcgr thm) ts
   29.99              #>> (fn (t, ts) => t `$$ ts)
  29.100 -and translate_eq thy algbr funcgr (thm, proper) =
  29.101 +and translate_eqn thy algbr funcgr (thm, proper) =
  29.102    let
  29.103      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
  29.104        o Logic.unvarify o prop_of) thm;