src/HOL/Tools/datatype_rep_proofs.ML
changeset 7704 9a6783fdb9a5
parent 7499 23e090051cb8
child 7904 2b551893583e
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Oct 04 21:45:10 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Oct 04 21:46:13 1999 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  
     1.5      (* make injections for constructors *)
     1.6  
     1.7 -    fun mk_univ_inj ts = access_bal (ap In0, ap In1, if ts = [] then
     1.8 +    fun mk_univ_inj ts = access_bal (fn t => In0 $ t, fn t => In1 $ t, if ts = [] then
     1.9          Const ("arbitrary", Univ_elT)
    1.10        else
    1.11          foldr1 (HOLogic.mk_binop Scons_name) ts);