src/ZF/intr_elim.ML
changeset 231 cb6a24451544
parent 202 4e68398cdc06
child 435 ca5356bd315a
equal deleted inserted replaced
230:ec8a2b6aa8a7 231:cb6a24451544
   102 (*** Extract basic information from arguments ***)
   102 (*** Extract basic information from arguments ***)
   103 
   103 
   104 val sign = sign_of Ind.thy;
   104 val sign = sign_of Ind.thy;
   105 
   105 
   106 fun rd T a = 
   106 fun rd T a = 
   107     Sign.read_cterm sign (a,T)
   107     read_cterm sign (a,T)
   108     handle ERROR => error ("The error above occurred for " ^ a);
   108     handle ERROR => error ("The error above occurred for " ^ a);
   109 
   109 
   110 val rec_names = map #1 rec_doms
   110 val rec_names = map #1 rec_doms
   111 and domts     = map (Sign.term_of o rd iT o #2) rec_doms;
   111 and domts     = map (term_of o rd iT o #2) rec_doms;
   112 
   112 
   113 val dummy = assert_all Syntax.is_identifier rec_names
   113 val dummy = assert_all Syntax.is_identifier rec_names
   114    (fn a => "Name of recursive set not an identifier: " ^ a);
   114    (fn a => "Name of recursive set not an identifier: " ^ a);
   115 
   115 
   116 val dummy = assert_all (is_some o lookup_const sign) rec_names
   116 val dummy = assert_all (is_some o lookup_const sign) rec_names
   117    (fn a => "Name of recursive set not declared as constant: " ^ a);
   117    (fn a => "Name of recursive set not declared as constant: " ^ a);
   118 
   118 
   119 val intr_tms = map (Sign.term_of o rd propT) sintrs;
   119 val intr_tms = map (term_of o rd propT) sintrs;
   120 
   120 
   121 local (*Checking the introduction rules*)
   121 local (*Checking the introduction rules*)
   122   val intr_sets = map (#2 o rule_concl) intr_tms;
   122   val intr_sets = map (#2 o rule_concl) intr_tms;
   123 
   123 
   124   fun intr_ok set =
   124   fun intr_ok set =