508     map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs

   508     map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs

   509 

   509 

   510   fun prep_bn env bn_str =

   510   fun prep_bn env bn_str =

   511     case (Syntax.read_term lthy bn_str) of

   511     case (Syntax.read_term lthy bn_str) of

   512        Free (x, _) => (NONE, env_lookup env x)

   512        Free (x, _) => (NONE, env_lookup env x)

   514      | _ => error (bn_str ^ " not allowed as binding specification.");  

   514      | _ => error (bn_str ^ " not allowed as binding specification.");  

   515  

   515  

   516   fun prep_typ env (i, opt_name) = 

   516   fun prep_typ env (i, opt_name) = 

   517     case opt_name of

   517     case opt_name of

   518       NONE => []

   518       NONE => []