src/Tools/nbe.ML
changeset 51685 385ef6706252
parent 48072 ace701efe203
child 52473 a2407f62a29f
     1.1 --- a/src/Tools/nbe.ML	Wed Apr 10 13:10:38 2013 +0200
     1.2 +++ b/src/Tools/nbe.ML	Wed Apr 10 15:30:19 2013 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4       of SOME T_class => T_class
     1.5        | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
     1.6      val tvar = case try Term.dest_TVar T
     1.7 -     of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
     1.8 +     of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort)
     1.9            then tvar
    1.10            else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
    1.11        | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
    1.12 @@ -65,11 +65,11 @@
    1.13      val lhs_rhs = case try Logic.dest_equals eqn
    1.14       of SOME lhs_rhs => lhs_rhs
    1.15        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
    1.16 -    val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
    1.17 +    val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
    1.18       of SOME c_c' => c_c'
    1.19        | _ => error ("Not an equation with two constants: "
    1.20            ^ Syntax.string_of_term_global thy eqn);
    1.21 -    val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
    1.22 +    val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
    1.23        else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
    1.24    in Triv_Class_Data.map (AList.update (op =) (class, thm)) thy end;
    1.25