equal
deleted
inserted
replaced
172 let |
172 let |
173 val ty = fastype_of x |
173 val ty = fastype_of x |
174 in |
174 in |
175 if arg_no mem args_in_bn then |
175 if arg_no mem args_in_bn then |
176 (if is_rec_type dt then |
176 (if is_rec_type dt then |
177 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good") |
177 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.") |
178 else @{term "{} :: atom set"}) else |
178 else @{term "{} :: atom set"}) else |
179 if is_atom thy ty then mk_single_atom x else |
179 if is_atom thy ty then mk_single_atom x else |
180 if is_atom_set thy ty then mk_atoms x else |
180 if is_atom_set thy ty then mk_atoms x else |
181 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
181 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
182 @{term "{} :: atom set"} |
182 @{term "{} :: atom set"} |
382 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
382 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
383 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
383 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
384 val fv_names_all = fv_names_fst @ fv_bn_names; |
384 val fv_names_all = fv_names_fst @ fv_bn_names; |
385 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
385 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
386 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
386 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
387 val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all) |
387 (* val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*) |
388 val (fvs, lthy') = (Primrec.add_primrec |
388 val (fvs, lthy') = (Primrec.add_primrec |
389 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
389 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
390 val (fvs2, lthy'') = |
390 val (fvs2, lthy'') = |
391 if fv_eqs_snd = [] then (([], []), lthy') else |
391 if fv_eqs_snd = [] then (([], []), lthy') else |
392 (Primrec.add_primrec |
392 (Primrec.add_primrec |
694 case try (find_index (curry op = tname o fst)) dts of |
694 case try (find_index (curry op = tname o fst)) dts of |
695 NONE => error "dtyp_no_of_typ: Illegal recursion" |
695 NONE => error "dtyp_no_of_typ: Illegal recursion" |
696 | SOME i => i |
696 | SOME i => i |
697 *} |
697 *} |
698 |
698 |
699 end |
699 ML {* |
|
700 fun rename_vars fnctn thm = |
|
701 let |
|
702 val vars = Term.add_vars (prop_of thm) [] |
|
703 val nvars = map (Var o ((apfst o apfst) fnctn)) vars |
|
704 in |
|
705 Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
|
706 end |
|
707 *} |
|
708 |
|
709 end |