src/HOL/Induct/LList.ML
changeset 10212 33fe2d701ddd
parent 10186 499637e8f2c6
child 10834 a7897aebbffc
     1.1 --- a/src/HOL/Induct/LList.ML	Thu Oct 12 18:09:06 2000 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Thu Oct 12 18:38:23 2000 +0200
     1.3 @@ -782,7 +782,7 @@
     1.4  by (ALLGOALS Asm_simp_tac);
     1.5  qed "fun_power_Suc";
     1.6  
     1.7 -val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
     1.8 +val Pair_cong = read_instantiate_sg (sign_of Product_Type.thy)
     1.9   [("f","Pair")] (standard(refl RS cong RS cong));
    1.10  
    1.11  (*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}