src/ZF/ind_syntax.ML
changeset 28965 1de908189869
parent 27261 5b3101338f42
child 30345 76fd85bbf139
     1.1 --- a/src/ZF/ind_syntax.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/ZF/ind_syntax.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -85,7 +85,7 @@
     1.4        Logic.list_implies
     1.5          (map FOLogic.mk_Trueprop prems,
     1.6  	 FOLogic.mk_Trueprop
     1.7 -	    (@{const mem} $ list_comb (Const (Sign.full_name sg name, T), args)
     1.8 +	    (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
     1.9  	               $ rec_tm))
    1.10    in  map mk_intr constructs  end;
    1.11