500     SOME x => x

   500     SOME x => x

   501   | NONE => error ("cannot find " ^ x ^ " in the binding specification.");

   501   | NONE => error ("cannot find " ^ x ^ " in the binding specification.");

   502 *}

   502 *}

   503 

   503 

   504 ML {*

   504 ML {*

   505 fun prepare_binds dt_strs lthy = 

   509 fun prepare_binds dt_strs lthy = 

   506 let

   510 let

   507   fun extract_annos_binds dt_strs =

   511   fun extract_annos_binds dt_strs =

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

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

   509 

   513 

   510   fun prep_bn env bn_str =

   514   fun prep_bn env bn_str =

   511     case (Syntax.read_term lthy bn_str) of

   515     case (Syntax.read_term lthy bn_str) of

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

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

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

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

   515  

   519  

   516   fun prep_typ env (i, opt_name) = 

   520   fun prep_typ env (i, opt_name) = 

   517     case opt_name of

   521     case opt_name of

   518       NONE => []

   522       NONE => []