src/HOL/Tools/record.ML
changeset 32749 3282c12a856c
parent 32748 887c68b70f7d
child 32752 f65d74a264dd
     1.1 --- a/src/HOL/Tools/record.ML	Fri Sep 11 18:03:30 2009 +1000
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Sep 11 20:58:29 2009 +1000
     1.3 @@ -1714,7 +1714,7 @@
     1.4                    asm_simp_tac HOL_ss 1]) end;
     1.5      val induct = timeit_msg "record extension induct proof:" induct_prf;
     1.6  
     1.7 -    val ([inject',induct',surjective',split_meta',ext_def'],
     1.8 +    val ([inject',induct',surjective',split_meta'],
     1.9        thm_thy) =
    1.10        defs_thy
    1.11        |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
    1.12 @@ -1723,7 +1723,7 @@
    1.13              ("ext_surjective", surject),
    1.14              ("ext_split", split_meta)]
    1.15  
    1.16 -  in (thm_thy,extT,induct',inject',split_meta',ext_def')
    1.17 +  in (thm_thy,extT,induct',inject',split_meta',ext_def)
    1.18    end;
    1.19  
    1.20  fun chunks []      []   = []