src/Pure/Isar/code.ML

          of SOME class => [TFree (Name.aT, [class])]
           | NONE => Name.invent_list [] Name.aT (length tvars)
               |> map (fn v => TFree (v, []));
         val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
       in raw_typscheme thy (c, ty) end
-  | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
+  | typscheme_eqns thy c (thm :: _) = typscheme_eqn thy thm;
 
 fun assert_eqns_const thy c eqns =
   let
     fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
       then eqn else error ("Wrong head of code equation,\nexpected constant "