src/HOL/Tools/record.ML
changeset 35408 b48ab741683b
parent 35363 09489d8ffece
child 35410 1ea89d2a1bd4
     1.1 --- a/src/HOL/Tools/record.ML	Sat Feb 27 22:52:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Feb 27 23:13:01 2010 +0100
     1.3 @@ -1100,7 +1100,7 @@
     1.4  fun get_accupd_simps thy term defset =
     1.5    let
     1.6      val (acc, [body]) = strip_comb term;
     1.7 -    val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
     1.8 +    val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
     1.9      fun get_simp upd =
    1.10        let
    1.11          (* FIXME fresh "f" (!?) *)