1065 SOME d => sort_defs prfx funs pfuns consts |
1065 SOME d => sort_defs prfx funs pfuns consts |
1066 (remove (op =) d defs) (d :: sdefs) |
1066 (remove (op =) d defs) (d :: sdefs) |
1067 | NONE => error ("Bad definitions: " ^ rulenames defs)); |
1067 | NONE => error ("Bad definitions: " ^ rulenames defs)); |
1068 |
1068 |
1069 fun set_vcs ({types, vars, consts, funs} : decls) |
1069 fun set_vcs ({types, vars, consts, funs} : decls) |
1070 (rules, _) ((_, ident), vcs) path prfx thy = |
1070 (rules, _) ((_, ident), vcs) path opt_prfx thy = |
1071 let |
1071 let |
|
1072 val prfx' = |
|
1073 if opt_prfx = "" then |
|
1074 space_implode "__" (Long_Name.explode (Long_Name.qualifier ident)) |
|
1075 else opt_prfx; |
|
1076 val prfx = to_lower prfx'; |
1072 val {pfuns, ...} = VCs.get thy; |
1077 val {pfuns, ...} = VCs.get thy; |
1073 val (defs, rules') = partition_opt dest_def rules; |
1078 val (defs, rules') = partition_opt dest_def rules; |
1074 val consts' = |
1079 val consts' = |
1075 subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts); |
1080 subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts); |
1076 (* ignore all complex rules in rls files *) |
1081 (* ignore all complex rules in rls files *) |
1092 ((Symtab.empty |> |
1097 ((Symtab.empty |> |
1093 Symtab.update ("false", (@{term False}, booleanN)) |> |
1098 Symtab.update ("false", (@{term False}, booleanN)) |> |
1094 Symtab.update ("true", (@{term True}, booleanN)), |
1099 Symtab.update ("true", (@{term True}, booleanN)), |
1095 Name.context), |
1100 Name.context), |
1096 thy |> Sign.add_path |
1101 thy |> Sign.add_path |
1097 ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |> |
1102 ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |> |
1098 fold (add_type_def prfx) (items types) |> |
1103 fold (add_type_def prfx) (items types) |> |
1099 fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) => |
1104 fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) => |
1100 ids_thy |> |
1105 ids_thy |> |
1101 fold_map (add_def prfx types pfuns consts) |
1106 fold_map (add_def prfx types pfuns consts) |
1102 (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>> |
1107 (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>> |