353 (** realizability predicate **) |
353 (** realizability predicate **) |
354 |
354 |
355 val (ind_info, thy3') = thy2 |> |
355 val (ind_info, thy3') = thy2 |> |
356 Inductive.add_inductive_global |
356 Inductive.add_inductive_global |
357 {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, |
357 {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, |
358 no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
358 no_elim = false, no_ind = false, skip_mono = false} |
359 rlzpreds rlzparams (map (fn (rintr, intr) => |
359 rlzpreds rlzparams (map (fn (rintr, intr) => |
360 ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), |
360 ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), |
361 subst_atomic rlzpreds' (Logic.unvarify_global rintr))) |
361 subst_atomic rlzpreds' (Logic.unvarify_global rintr))) |
362 (rintrs ~~ maps snd rss)) [] ||> |
362 (rintrs ~~ maps snd rss)) [] ||> |
363 Sign.root_path; |
363 Sign.root_path; |