src/HOL/Tools/SMT2/smt2_builtin.ML

 
 (* built-in tables *)
 
 datatype ('a, 'b) kind = Ext of 'a | Int of 'b
 
-type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict 
+type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict
 
 fun typ_ord ((T, _), (U, _)) =
   let
     fun tord (TVar _, Type _) = GREATER
       | tord (Type _, TVar _) = LESS

   lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
 
 fun dest_builtin_typ ctxt T =
   (case lookup_builtin_typ ctxt T of
     SOME (_, Int (f, _)) => f T
-  | _ => NONE) 
+  | _ => NONE)
 
 fun is_builtin_typ_ext ctxt T =
   (case lookup_builtin_typ ctxt T of
     SOME (_, Int (f, _)) => is_some (f T)
   | SOME (_, Ext f) => f T

     (case dest_builtin_num ctxt t of
       SOME (n, _) => SOME (n, 0, [], K t)
     | NONE => dest_builtin_fun ctxt c ts)
   end
 
-fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
+fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =
   (case lookup_builtin_fun ctxt c of
     SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
   | SOME (_, Ext f) => SOME (f ctxt T ts)
   | NONE => NONE)