TFL/tfl.sml
changeset 3927 27c63b757af5
parent 3768 67f4ac759100
child 3944 8988ba66c62b
equal deleted inserted replaced
3926:f5e499fda22c 3927:27c63b757af5
   217                                       rows = ListPair.zip (pat_rectangle',
   217                                       rows = ListPair.zip (pat_rectangle',
   218                                                            rights')}
   218                                                            rights')}
   219           in (map v_to_pats pref_patl, tm)
   219           in (map v_to_pats pref_patl, tm)
   220           end
   220           end
   221      else
   221      else
   222      let val pty as Type (ty_name,_) = type_of p
   222      let val pty as Type (full_ty_name,_) = type_of p;
       
   223          val ty_name = NameSpace.base full_ty_name;
   223      in
   224      in
   224      case (ty_info ty_name)
   225      case (ty_info ty_name)
   225      of None => mk_case_fail("Not a known datatype: "^ty_name)
   226      of None => mk_case_fail("Not a known datatype: "^ty_name)
   226       | Some{case_const,constructors} =>
   227       | Some{case_const,constructors} =>
   227         let val case_const_name = #1(dest_Const case_const)
   228         let val case_const_name = #1(dest_Const case_const)
   297      val originals = map (row_of_pat o #2) rows
   298      val originals = map (row_of_pat o #2) rows
   298      val dummy = case (originals\\finals)
   299      val dummy = case (originals\\finals)
   299              of [] => ()
   300              of [] => ()
   300           | L => mk_functional_err("The following rows (counting from zero)\
   301           | L => mk_functional_err("The following rows (counting from zero)\
   301                                    \ are inaccessible: "^stringize L)
   302                                    \ are inaccessible: "^stringize L)
   302  in {functional = Abs(fname, ftype, 
   303  in {functional = Abs(NameSpace.base fname, ftype,
   303 		      abstract_over (fcon, 
   304 		      abstract_over (fcon, 
   304 				     absfree(aname,atype, case_tm))),
   305 				     absfree(aname,atype, case_tm))),
   305      pats = patts2}
   306      pats = patts2}
   306 end end;
   307 end end;
   307 
   308 
   549      then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
   550      then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
   550                                 (ListPair.zip (rights, col0))
   551                                 (ListPair.zip (rights, col0))
   551           in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
   552           in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
   552           end
   553           end
   553      else                     (* column 0 is all constructors *)
   554      else                     (* column 0 is all constructors *)
   554      let val Type (ty_name,_) = type_of p
   555      let val Type (full_ty_name,_) = type_of p;
       
   556          val ty_name = NameSpace.base full_ty_name;
   555      in
   557      in
   556      case (ty_info ty_name)
   558      case (ty_info ty_name)
   557      of None => fail("Not a known datatype: "^ty_name)
   559      of None => fail("Not a known datatype: "^ty_name)
   558       | Some{constructors,nchotomy} =>
   560       | Some{constructors,nchotomy} =>
   559         let val thm' = R.ISPEC (tych u) nchotomy
   561         let val thm' = R.ISPEC (tych u) nchotomy